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

NAME

6       e_axfilter - manual page for e_axfilter 2.3-DEBUG Gielle
7

SYNOPSIS

9       e_axfilter [options] [files]
10

DESCRIPTION

12       e_axfilter 2.3-DEBUG "Gielle"
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
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

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 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
54       -o <arg>
55
56       --output-file=<arg>
57
58              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
62       -s
63
64       --silent
65
66              Equivalent to --output-level=0.
67
68       -l <arg>
69
70       --output-level=<arg>
71
72              Select an output level, greater values imply more  verbose  out‐
73              put.
74
75       -f <arg>
76
77       --filter=<arg>
78
79              Specify  the filter definition file. If not set, the system will
80              uses the built-in default.
81
82       -S
83
84       --seed-symbols[=<arg>]
85
86              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
95       --seed-subsample[=<arg>]
96
97              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
105       -m
106
107       --seed-method[=<arg>]
108
109              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
121       -d
122
123       --dump-filter
124
125              Print the filter definition in force.
126
127       --lop-in
128
129              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
135       --lop-format
136
137              Equivalent to --lop-in.
138
139       --tptp-in
140
141              Parse TPTP-2 format instead of E-LOP (but note that includes are
142              handled according to TPTP-3 semantics).
143
144       --tptp-format
145
146              Equivalent to --tptp-in.
147
148       --tptp2-in
149
150              Synonymous with --tptp-in.
151
152       --tptp2-format
153
154              Synonymous with --tptp-in.
155
156       --tstp-in
157
158              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
163       --tstp-format
164
165              Equivalent to --tstp-in.
166
167       --tptp3-in
168
169              Synonymous with --tstp-in.
170
171       --tptp3-format
172
173              Synonymous with --tstp-in.
174

REPORTING BUGS

176       Report  bugs  to <schulz@eprover.org>. Please include the following, if
177       possible:
178
179       * The version of the package as reported by eprover --version.
180
181       * The operating system and version.
182
183       * The exact command line that leads to the unexpected behaviour.
184
185       * A description of what you expected and what actually happend.
186
187       * 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
193       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
197       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
202       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
207       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
213       The original copyright holder can be contacted via email or as
214
215       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
216       buehlplatz 41 70178 Stuttgart Germany
217
218
219
220e_axfilter 2.3-DEBUG Gielle       April 2019                     E_AXFILTER(1)
Impressum