Provided by: eprover_2.6+ds-3_amd64 
NAME
e_axfilter - manual page for e_axfilter 2.6 Floral Guranse
SYNOPSIS
e_axfilter [options] [files]
DESCRIPTION
e_axfilter 2.6 "Floral Guranse"
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.
--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-2021 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 Rotebuehlplatz 41 70178
Stuttgart Germany