Ubuntu Manpage: e_axfilter - manual page for e_axfilter 3.0.03-DEBUG Shangri-La

NAME

       e_axfilter - manual page for e_axfilter 3.0.03-DEBUG Shangri-La

SYNOPSIS

       e_axfilter [options] [files]

DESCRIPTION

       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

OPTIONS

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

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 happened.

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

COPYRIGHT

       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

e_axfilter 3.0.03-DEBUG Shangri-La                December 2023                                    E_AXFILTER(1)