e_axfilter - manual page for e_axfilter 3.0.03-DEBUG
Shangri-La
e_axfilter [options] [files]
e_axfilter 3.0.03-DEBUG "Shangri-La"
This program applies SinE-like goal-directed filters to a problem
specification (a set of clauses and/or formulas) to generate reduced problem
specifications that are easier to handle for a theorem prover, but still are
likely to contain all the axioms necessary for a proof (if one exists).
In default mode, the program reads a problem specification and an
(optional) filter specification, and produces one reduced output file for
each filter given. Note that while all standard input formats (LOP, TPTP-2
and TPTP-3 are supported, output is only and automatically in 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
-h
--help
- Print a short description of program usage and options.
-V
--version
- Print the version number of the prover. Please include this with all bug
reports (if any).
-v
--verbose[=<arg>]
- Verbose comments on the progress of the program. This technical
information is printed to stderr. The short form or the long form without
the optional argument is equivalent to --verbose=1.
-o <arg>
--output-file=<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.
-s
--silent
- Equivalent to --output-level=0.
-l <arg>
--output-level=<arg>
- Select an output level, greater values imply more verbose output.
-f <arg>
--filter=<arg>
- Specify the filter definition file. If not set, the system will uses the
built-in default.
-S
--seed-symbols[=<arg>]
- Enable artificial seeding of the axiom selection process and determine
which symbol classes should be used to generate different sets.The
argument is a string of letters, each indicating one class of symbols to
use. 'p' indicates predicate symbols, 'f' non-constant function symbols,
and 'c' constants. Note that this will create potentially multiple output
files for each activated symbols. The short form or the long form without
the optional argument is equivalent to
--seed-symbols=p.
--seeds=<arg>
- Explicitly specify the symbols that should be used as seed symbols for
axiom extraction. This overwrites --seed-subsample and
--seed-symbols.
--seed-subsample[=<arg>]
- Subsample from the set of eligible seed symbols. The argument is a
one-character designator for the method ('m' uses the symbols that occur
in the most input formulas, 'l' uses the symbols that occur in the least
number of formulas, and 'r' samples randomly), followed by the number of
symbols to select. The option without the optional argument is equivalent
to --seed-subsample=r1000.
-m
--seed-method[=<arg>]
- Specify how to select seed axioms when artificially seeding is used.The
argument is a string of letters, each indicating one method to use. The
letters are: 'l': use the syntactically largest axiom in which the seed
symbol occurs. 'd': use the most diverse axiom in which the seed symbol
occurs, i.e. the symbol with the largest set of different symbols. 'a':
use all axioms in which the seed symbol occurs. For 'l' and 'd', if there
are multiple candidates, use the first one.If the option is not set, 'a'
is assumed. The short form or the long form without the optional argument
is equivalent to --seed-method=lda.
-d
--dump-filter
- Print the filter definition in force.
--lop-in
- 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.
--lop-format
- Equivalent to --lop-in.
--tptp-in
- Parse TPTP-2 format instead of E-LOP (but note that includes are handled
according to TPTP-3 semantics).
--tptp-format
- Equivalent to --tptp-in.
--tptp2-in
- Synonymous with --tptp-in.
--tptp2-format
- Synonymous with --tptp-in.
--tstp-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).
--tstp-format
- Equivalent to --tstp-in.
--tptp3-in
- Synonymous with --tstp-in.
--tptp3-format
- Synonymous with --tstp-in.
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
happened.
* If possible all input files necessary to reproduce the bug.
Copyright 1998-2023 by Stephan Schulz, schulz@eprover.org, and the
E contributors (see DOC/CONTRIBUTORS).
This program is a part of the distribution of the equational
theorem prover E. You can find the latest version of the E distribution as
well as additional information at http://www.eprover.org
This program is free software; you can redistribute it and/or
modify it under the terms of the GNU General Public License as published by
the Free Software Foundation; either version 2 of the License, or (at your
option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
Public License for more details.
You should have received a copy of the GNU General Public License
along with this program (it should be contained in the top level directory
of the distribution in the file COPYING); if not, write to the Free Software
Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA 02111-1307 USA
The original copyright holder can be contacted via email or as
Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
Lerchenstrasse 1 70174 Stuttgart Germany