e_axfilter

E_AXFILTER(1)                    User Commands                   E_AXFILTER(1)



NAME
       e_axfilter - manual page for e_axfilter 1.9 Sourenee

SYNOPSIS
       e_axfilter [options] [files]

DESCRIPTION
       e_axfilter 1.9 "Sourenee"

       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

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

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

       -d

       --dump-filter

              Print the filter definition in force.

       --lop-in

              Parse input in E-LOP, not the default TPTP-3 format.

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

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

COPYRIGHT
       Copyright 1998-2014 by Stephan Schulz, schulz@eprover.org

       You can find the latest version of E and 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 as

       Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
       Rotebuehlplatz 41 70178 Stuttgart Germany



e_axfilter 1.9 Sourenee            July 2015                     E_AXFILTER(1)