Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages


home | help
E_AXFILTER(1)			 User Commands			 E_AXFILTER(1)

       e_axfilter - manual page	for e_axfilter 2.0 Turzum

       e_axfilter [options] [files]

       e_axfilter 2.0 "Turzum"

       This program applies SinE-like goal-directed filters to a problem spec-
       ification (a set	of clauses and/or formulas) to generate	reduced	 prob-
       lem  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  dfault  mode, the program reads a problem specification and an (op-
       tional) 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 distri-
       bution, 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 logi-
	      cal 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 out-
	      put,  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  out-

       -f <arg>


	      Specify  the filter definition file. If not set, the system will
	      uses the built-in	default.



	      Enable artificial	seeding	of the axiom selection process and de-
	      termine  which symbol classes should be used to generate differ-
	      ent 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 ac-
	      tivated symbols. The short form or the long form without the op-
	      tional argument is equivalent to --seed-symbols=p.


	      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  ran-
	      domly),  followed	by the number of symbols to select. The	option
	      without the optional argument is	equivalent  to	--seed-subsam-



	      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



	      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.

       Report  bugs  to	<>. Please include the following, if

       * 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 1998-2017 by Stephan Schulz,,  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

       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 MER-
       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 Soft-
       ware  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	 Rote-
       buehlplatz 41 70178 Stuttgart Germany

e_axfilter 2.0 Turzum		  August 2020			 E_AXFILTER(1)


Want to link to this manual page? Use this URL:

home | help