1E_AXFILTER(1)                    User Commands                   E_AXFILTER(1)
2
3
4

NAME

6       e_axfilter - manual page for e_axfilter 2.6-DEBUG Floral Guranse
7

SYNOPSIS

9       e_axfilter [options] [files]
10

DESCRIPTION

12       e_axfilter 2.6-DEBUG "Floral Guranse"
13
14       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
20       In  default mode, the program reads a problem specification and an (op‐
21       tional) filter specification, and produces one reduced output file  for
22       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

OPTIONS

30       -h
31
32       --help
33
34              Print a short description of program usage and options.
35
36       -V
37
38       --version
39
40              Print the version number of the prover. Please include this with
41              all bug reports (if any).
42
43       -v
44
45       --verbose[=<arg>]
46
47              Verbose  comments on the progress of the program. This technical
48              information is printed to stderr. The short  form  or  the  long
49              form without the optional argument is equivalent to --verbose=1.
50
51       -o <arg>
52
53       --output-file=<arg>
54
55              Redirect output into the named file (this affects only some out‐
56              put, as most is written to automatically generated  files  based
57              on the input and filter names.
58
59       -s
60
61       --silent
62
63              Equivalent to --output-level=0.
64
65       -l <arg>
66
67       --output-level=<arg>
68
69              Select  an  output level, greater values imply more verbose out‐
70              put.
71
72       -f <arg>
73
74       --filter=<arg>
75
76              Specify the filter definition file. If not set, the system  will
77              uses the built-in default.
78
79       -S
80
81       --seed-symbols[=<arg>]
82
83              Enable artificial seeding of the axiom selection process and de‐
84              termine which symbol classes should be used to generate  differ‐
85              ent  sets.The  argument  is a string of letters, each indicating
86              one class of symbols to use. 'p'  indicates  predicate  symbols,
87              'f'  non-constant function symbols, and 'c' constants. Note that
88              this will create potentially multiple output files for each  ac‐
89              tivated symbols. The short form or the long form without the op‐
90              tional argument is equivalent to --seed-symbols=p.
91
92       --seed-subsample[=<arg>]
93
94              Subsample from the set of eligible seed symbols. The argument is
95              a  one-character designator for the method ('m' uses the symbols
96              that occur in the most input formulas, 'l' uses the symbols that
97              occur  in  the  least  number  of formulas, and 'r' samples ran‐
98              domly), followed by the number of symbols to select. The  option
99              without  the  optional  argument is equivalent to --seed-subsam‐
100              ple=r1000.
101
102       -m
103
104       --seed-method[=<arg>]
105
106              Specify how to select seed axioms when artificially  seeding  is
107              used.The  argument  is  a string of letters, each indicating one
108              method to use. The  letters  are:  'l':  use  the  syntactically
109              largest  axiom  in  which  the seed symbol occurs.  'd': use the
110              most diverse axiom in which the seed  symbol  occurs,  i.e.  the
111              symbol  with the largest set of different symbols.  'a': use all
112              axioms in which the seed symbol occurs.  For  'l'  and  'd',  if
113              there  are  multiple candidates, use the first one.If the option
114              is not set, 'a' is assumed. The short  form  or  the  long  form
115              without    the    optional    argument    is    equivalent    to
116              --seed-method=lda.
117
118       -d
119
120       --dump-filter
121
122              Print the filter definition in force.
123
124       --lop-in
125
126              Set E-LOP as the input format. If no input format is selected by
127              this  or  one  of  the following options, E will guess the input
128              format based on the first token. It will almost always correctly
129              recognize  TPTP-3,  but  it may misidentify E-LOP files that use
130              TPTP meta-identifiers as logical symbols.
131
132       --lop-format
133
134              Equivalent to --lop-in.
135
136       --tptp-in
137
138              Parse TPTP-2 format instead of E-LOP (but note that includes are
139              handled according to TPTP-3 semantics).
140
141       --tptp-format
142
143              Equivalent to --tptp-in.
144
145       --tptp2-in
146
147              Synonymous with --tptp-in.
148
149       --tptp2-format
150
151              Synonymous with --tptp-in.
152
153       --tstp-in
154
155              Parse TPTP-3 format instead of E-LOP (Note that TPTP-3 syntax is
156              still under development, and the version in E may not  be  fully
157              conforming  at  all times. E works on all TPTP 6.3.0 FOF and CNF
158              input files (including includes).
159
160       --tstp-format
161
162              Equivalent to --tstp-in.
163
164       --tptp3-in
165
166              Synonymous with --tstp-in.
167
168       --tptp3-format
169
170              Synonymous with --tstp-in.
171

REPORTING BUGS

173       Report bugs to <schulz@eprover.org>. Please include the  following,  if
174       possible:
175
176       * The version of the package as reported by eprover --version.
177
178       * The operating system and version.
179
180       * The exact command line that leads to the unexpected behaviour.
181
182       * A description of what you expected and what actually happend.
183
184       * If possible all input files necessary to reproduce the bug.
185
187       Copyright  1998-2021  by  Stephan Schulz, schulz@eprover.org, and the E
188       contributors (see DOC/CONTRIBUTORS).
189
190       This program is a part of the distribution of  the  equational  theorem
191       prover E. You can find the latest version of the E distribution as well
192       as additional information at http://www.eprover.org
193
194       This program is free software; you can redistribute it and/or modify it
195       under  the  terms of the GNU General Public License as published by the
196       Free Software Foundation; either version 2 of the License, or (at  your
197       option) any later version.
198
199       This  program  is  distributed  in the hope that it will be useful, but
200       WITHOUT ANY  WARRANTY;  without  even  the  implied  warranty  of  MER‐
201       CHANTABILITY  or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
202       Public License for more details.
203
204       You should have received a copy of the GNU General Public License along
205       with this program (it should be contained in the top level directory of
206       the distribution in the file COPYING); if not, write to the Free  Soft‐
207       ware   Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,  MA
208       02111-1307 USA
209
210       The original copyright holder can be contacted via email or as
211
212       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
213       buehlplatz 41 70178 Stuttgart Germany
214
215
216
217e_axfilter 2.6-DEBUG Floral GuranseJuly 2023                     E_AXFILTER(1)
Impressum