e_axfilter man page

e_axfilter — manual page for e_axfilter 1.9.1-001 Sungma


e_axfilter [options] [files]


e_axfilter 1.9.1-001 "Sungma"

This problem applies SinE-like goal-directed filters to a problem specification to generate reduced problem specifications that are easier to handle for the prover, but still are likely to contain the necessary axioms for a proof (if one exists). The program reads a problem specification and a filter specification, and produces one reduced specifiation for each filter given. Note that while all input formats (LOP, TPTP-2 and TPTP-3 are supported, output is only and automatically supported in TPTP-3, and the default input format is TPTP-3. Also note that unlike most of the other tools in the E distribution, this program does not support pipe-based input and output, since it uses file names generated from the input file name and filter names to store the different result files


Print a short description of program usage and options.
Print the version number of the prover. Please include this with all bug reports (if any).
Verbose comments on the progress of the program. This differs from the output level (below) in that technical information is printed to stderr, while the output level determines which logical manipulations of the clauses are printed to stdout. The short form or the long form without the optional argument is equivalent to --verbose=1.
-o <arg>
Redirect output into the named file (this affects only some output, as most is written to automatically generated files based on the input and filter names.
Equivalent to --output-level=0.
-l <arg>
Select an output level, greater values imply more verbose output.
-f <arg>
Specify the filter definition file. If not set, the system will uses the built-in default.
Print the filter definition in force.
Set E-LOP as the input format. If no input format is selected by this or one of the following options, E will guess the input format based on the first token. It will almost always correctly recognize TPTP-3, but it may misidentify E-LOP files that use TPTP meta-identifiers as logical symbols.
Equivalent to --lop-in.
Parse TPTP-2 format instead of E-LOP (but note that includes are handled according to TPTP-3 semantics).
Equivalent to --tptp-in.
Synonymous with --tptp-in.
Synonymous with --tptp-in.
Parse TPTP-3 format instead of E-LOP (Note that TPTP-3 syntax is still under development, and the version in E may not be fully conforming at all times. E works on all TPTP 6.3.0 FOF and CNF input files (including includes).
Equivalent to --tstp-in.
Synonymous with --tstp-in.
Synonymous with --tstp-in.

Reporting Bugs

Report bugs to <schulz@eprover.org>. Please include the following, if possible:

* The version of the package as reported by eprover --version.

* The operating system and version.

* The exact command line that leads to the unexpected behaviour.

* A description of what you expected and what actually happend.

* If possible all input files necessary to reproduce the bug.


February 2017 e_axfilter 1.9.1-001 Sungma User Commands