1E_AXFILTER(1) User Commands E_AXFILTER(1)
2
6 e_axfilter - manual page for e_axfilter 2.3-DEBUG Gielle
7
9 e_axfilter [options] [files]
10
12 e_axfilter 2.3-DEBUG "Gielle"
13 This program applies SinE-like goal-directed filters to a problem spec‐
15 ification (a set of clauses and/or formulas) to generate reduced prob‐
16 lem specifications that are easier to handle for a theorem prover, but
17 still are likely to contain all the axioms necessary for a proof (if
18 one exists).
19 In default mode, the program reads a problem specification and an
21 (optional) filter specification, and produces one reduced output file
22 for each filter given. Note that while all standard input formats (LOP,
23 TPTP-2 and TPTP-3 are supported, output is only and automatically in
24 TPTP-3. Also note that unlike most of the other tools in the E distri‐
25 bution, this program does not support pipe-based input and output,
26 since it uses file names generated from the input file name and filter
27 names to store the different result files
28
30 -h
31 --help
33 Print a short description of program usage and options.
35 -V
37 --version
39 Print the version number of the prover. Please include this with
41 all bug reports (if any).
42 -v
44 --verbose[=<arg>]
46 Verbose comments on the progress of the program. This differs
48 from the output level (below) in that technical information is
49 printed to stderr, while the output level determines which logi‐
50 cal manipulations of the clauses are printed to stdout. The
51 short form or the long form without the optional argument is
52 equivalent to --verbose=1.
53 -o <arg>
55 --output-file=<arg>
57 Redirect output into the named file (this affects only some out‐
59 put, as most is written to automatically generated files based
60 on the input and filter names.
61 -s
63 --silent
65 Equivalent to --output-level=0.
67 -l <arg>
69 --output-level=<arg>
71 Select an output level, greater values imply more verbose out‐
73 put.
74 -f <arg>
76 --filter=<arg>
78 Specify the filter definition file. If not set, the system will
80 uses the built-in default.
81 -S
83 --seed-symbols[=<arg>]
85 Enable artificial seeding of the axiom selection process and
87 determine which symbol classes should be used to generate dif‐
88 ferent sets.The argument is a string of letters, each indicating
89 one class of symbols to use. 'p' indicates predicate symbols,
90 'f' non-constant function symbols, and 'c' constants. Note that
91 this will create potentially multiple output files for each
92 activated symbols. The short form or the long form without the
93 optional argument is equivalent to --seed-symbols=p.
94 --seed-subsample[=<arg>]
96 Subsample from the set of eligible seed symbols. The argument is
98 a one-character designator for the method ('m' uses the symbols
99 that occur in the most input formulas, 'l' uses the symbols that
100 occur in the least number of formulas, and 'r' samples ran‐
101 domly), followed by the number of symbols to select. The option
102 without the optional argument is equivalent to --seed-subsam‐
103 ple=r1000.
104 -m
106 --seed-method[=<arg>]
108 Specify how to select seed axioms when artificially seeding is
110 used.The argument is a string of letters, each indicating one
111 method to use. The letters are: 'l': use the syntactically
112 largest axiom in which the seed symbol occurs. 'd': use the
113 most diverse axiom in which the seed symbol occurs, i.e. the
114 symbol with the largest set of different symbols. 'a': use all
115 axioms in which the seed symbol occurs. For 'l' and 'd', if
116 there are multiple candidates, use the first one.If the option
117 is not set, 'a' is assumed. The short form or the long form
118 without the optional argument is equivalent to
119 --seed-method=lda.
120 -d
122 --dump-filter
124 Print the filter definition in force.
126 --lop-in
128 Set E-LOP as the input format. If no input format is selected by
130 this or one of the following options, E will guess the input
131 format based on the first token. It will almost always correctly
132 recognize TPTP-3, but it may misidentify E-LOP files that use
133 TPTP meta-identifiers as logical symbols.
134 --lop-format
136 Equivalent to --lop-in.
138 --tptp-in
140 Parse TPTP-2 format instead of E-LOP (but note that includes are
142 handled according to TPTP-3 semantics).
143 --tptp-format
145 Equivalent to --tptp-in.
147 --tptp2-in
149 Synonymous with --tptp-in.
151 --tptp2-format
153 Synonymous with --tptp-in.
155 --tstp-in
157 Parse TPTP-3 format instead of E-LOP (Note that TPTP-3 syntax is
159 still under development, and the version in E may not be fully
160 conforming at all times. E works on all TPTP 6.3.0 FOF and CNF
161 input files (including includes).
162 --tstp-format
164 Equivalent to --tstp-in.
166 --tptp3-in
168 Synonymous with --tstp-in.
170 --tptp3-format
172 Synonymous with --tstp-in.
174
176 Report bugs to <schulz@eprover.org>. Please include the following, if
177 possible:
178 * The version of the package as reported by eprover --version.
180 * The operating system and version.
182 * The exact command line that leads to the unexpected behaviour.
184 * A description of what you expected and what actually happend.
186 * If possible all input files necessary to reproduce the bug.
188
190 Copyright 1998-2019 by Stephan Schulz, schulz@eprover.org, and the E
191 contributors (see DOC/CONTRIBUTORS).
192 This program is a part of the distribution of the equational theorem
194 prover E. You can find the latest version of the E distribution as well
195 as additional information at http://www.eprover.org
196 This program is free software; you can redistribute it and/or modify it
198 under the terms of the GNU General Public License as published by the
199 Free Software Foundation; either version 2 of the License, or (at your
200 option) any later version.
201 This program is distributed in the hope that it will be useful, but
203 WITHOUT ANY WARRANTY; without even the implied warranty of MER‐
204 CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
205 Public License for more details.
206 You should have received a copy of the GNU General Public License along
208 with this program (it should be contained in the top level directory of
209 the distribution in the file COPYING); if not, write to the Free Soft‐
210 ware Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
211 02111-1307 USA
212 The original copyright holder can be contacted via email or as
214 Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Rote‐
216 buehlplatz 41 70178 Stuttgart Germany
217e_axfilter 2.3-DEBUG Gielle April 2019 E_AXFILTER(1)