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 lengthy formal document.

About XSLT

Why are there two XSLT files in the source code for the translation?

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 that we can utilize. The normailizer we use in this project is actually the one for a super set of Datalog+, however it goes well along with this project.

About Java Source Code

Why is there only one Java source code file in 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 a normalization step as 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.

Is there documentation for the Java source code?

No. The Java code is quite straightforward. The comments in it should be enough for reading it.

About Program Options

How can I remember how to use the program?

Try "java -jar ruleml2tptp.tar -h" at first.

What does option -r do?

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.

How can I get a look at the normalized RuleML?

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.

How can I retains comments in the output from the source file?

Use -c. If a pattern in regular expression follows, only comments which content match the pattern will be carried into the output.

How can I keep only part of a comment?

Write that comment into two parts. Use -c to distinguish them.

What kind of regular expression does this program use?

The regular expression will be used directly with XPath functions. See XPath functions specification for the syntax.

What are the flags with -g?

See XPath functions specification for the flags. Basically "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 entire 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.

Why do I get warnings about variables or constants?

It is because the variables, constants and functors must follow the TPTP language syntax. RuleML2TPTP tries to convert alphabetic case of the first letter, or to single quote variables, constants and functors in RuleML to make them valid in the TPTP language. However, they can still be not valid after the conversion. That is when the warnings are issued.

Why don't I get the warnings when there are invalid variables, constants and functors even after the conversion?

When, for example, the output and the standard error are both to print on the screen, warnings can be suppressed to avoid messing up the output. Redirecting and separating them will bring up the warnings.

How are the comments converted into the TPTP syntax?

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
%----------------------------------

Why can't I keep the comments in <Atom>?

Because it usually is not a good idea to break a TPTP formula with comments. Only comments outside a TPTP formula, that is, at most as deep as the child nodes of <Assert> and <Query>, can be retained.

About Saxon

Can I use other JAXP implementation instead of Saxon?

Yes. The java library file saxon.jar can be removed, and then the local implementation will be used. Alternatively, option -t can be used to specify a third party transformer factory class. Remember to put that class under the class path. Whichever implementation is about to use, this project uses a XSLT 2.0 normalizer and translator, so make sure the implementation supports XSLT 2.0.

How can I tell which implementation I am using and whether it supports XSLT 2.0?

Use option -h.