Repository navigation
FAQ
Welcome to the RuleML2TPTP FAQ! This page also serves as the supporting and flexible documentation characterized by brisk questions and answers. We think that this form is better for this project than a lenghy formal document.
One is to normalize the source RuleML file, and the other is for the real translation. RuleML allows abbreviated encoding (skipped edge tags and default attribute values) and some freedom in the ordering of elements. It would be much easier to do translation on normalized RuleML than the original (un-normalized) source. Moreover, RuleML has provided normalizers in XSLT. The normailizer we use in this project is actually for a superset of Datalog+, however it goes well along this project.
Because it is enough. The only Java class (the main class) is to parse the command line arguments and translate the input as to the parsed options by invoking JAXP calls.
Why do you bother with Java code to do? Why not just use shell script as Saxon is executable, or call Saxon directly?
Our translation has normalization as the pre-processing. Calling Saxon directly is full of typing and memorizing. We tried shell script but it is platform- (or shell-) dependent. Then we found we preferred more to a platform-independent solution.
No. The Java code is quite straightforward. The comments in it should be enough for reading it.
Try "java -jar ruleml2tptp.tar -h" at first.
With this option, CRLF will be used to mark new lines in the output translation (like on Windows OS) instead of the default LF only.
Use -nt, which suppresses the real translation and retains the normalization. The output will become the result of normalization. If the result is saved in a file, later it can be used as the source with option -nn, so that normalization will not be done again.
Use -c. If a pattern in regular expression follows, only comments which content match the pattern will be carried into the output.
Write that comment into two parts. Use -c to distinguish them.
The regular expression will be used directly with XPath functions. See XPath functions specification for the syntax.
See XPath functions specification for the flags. Basicaly "i" means case-insensitive mode, "s" means that dot can match the newline character, and "m" means multi-line mode where ^ and $ match the start and end of a line instead of the entired input string. "v" is specific to this program, meaning not to select the comments that match the pattern, but to select those that do not match the pattern. It is like "grep -v" on UNIX/Linux.
Generally speaking, "%" followed by a space will be added in at the beginning of each line after the line has been trimmed clear of leading and trailing whitespace. If a trimmed line starts with "-- " (two dashes followed by a space), "--" will be replaced by "%". This can be used to keep the indentation in the original comments. If a line has only dashes, only "%" will be inserted at the beginning. A line starts with "%" will not be changed. Here is an example comment:
<!-- An example comment:
-- Indent
% A percent sign starts a comment line.
-- %100 keep this
------------------------------------>
It will be converted into the following:
% An example comment:
% Indent
% A percent sign starts a comment line.
% %100 keep this
%----------------------------------
Because it usually is not a good idea to break a TPTP formula with comments. Only commments outside a TPTP formula, that is, at most as deep as the children nodes of <Assert> and <Query>, can be retained.