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

NAME

6       epclextract - manual page for epclextract 2.5-DEBUG
7

SYNOPSIS

9       epclextract [options] [files]
10

DESCRIPTION

12       epclextract 2.5-DEBUG
13
14       Read  an  PCL2  protocol  and print the steps necessary for proving the
15       clauses in "proof", "final", or "extract" steps.
16
17       Options
18
19       -h
20
21       --help
22
23              Print a short description of program usage and options.
24
25       -V
26
27       --version
28
29              Print the version number of the program.
30
31       -v
32
33       --verbose[=<arg>]
34
35              Verbose comments on the progress of the program. The short  form
36              or  the long form without the optional argument is equivalent to
37              --verbose=1.
38
39       -f
40
41       --fast-extract
42
43              Do a fast extract. With this option the program understands only
44              a  subset  of PCL and assumes that all "proof" and "final" steps
45              are at the end of the protocoll.
46
47       -C
48
49       --forward-comments
50
51              Pass comments found in the input through  to  the  output  while
52              reading input.
53
54       -c
55
56       --competition-framing
57
58              Print special "begin" and "end"comments around the proof object,
59              as requiered by the CASC MIX* class.
60
61       -n
62
63       --no-extract
64
65              Don't extract, print back all steps  (actually,  it  treats  all
66              steps  as  proof  steps).  Useful as a syntax checker, or if you
67              want to convert PCL to TSTP with the next option.
68
69       --tstp-out
70
71              Print proof protocol in TSTP syntax (default is PCL).
72
73       --tptp3-out
74
75              Synonymous with --tstp-out.
76
77       -o <arg>
78
79       --output-file=<arg>
80
81              Redirect output into the named file.
82
83       -s
84
85       --silent
86
87              Equivalent to --output-level=0.
88

REPORTING BUGS

90       Report bugs to <schulz@eprover.org>. Please include the  following,  if
91       possible:
92
93       * The version of the package as reported by eprover --version.
94
95       * The operating system and version.
96
97       * The exact command line that leads to the unexpected behaviour.
98
99       * A description of what you expected and what actually happend.
100
101       * If possible all input files necessary to reproduce the bug.
102

104       Copyright  1998-2020  by  Stephan Schulz, schulz@eprover.org, and the E
105       contributors (see DOC/CONTRIBUTORS).
106
107       This program is a part of the distribution of  the  equational  theorem
108       prover E. You can find the latest version of the E distribution as well
109       as additional information at http://www.eprover.org
110
111       This program is free software; you can redistribute it and/or modify it
112       under  the  terms of the GNU General Public License as published by the
113       Free Software Foundation; either version 2 of the License, or (at  your
114       option) any later version.
115
116       This  program  is  distributed  in the hope that it will be useful, but
117       WITHOUT ANY  WARRANTY;  without  even  the  implied  warranty  of  MER‐
118       CHANTABILITY  or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
119       Public License for more details.
120
121       You should have received a copy of the GNU General Public License along
122       with this program (it should be contained in the top level directory of
123       the distribution in the file COPYING); if not, write to the Free  Soft‐
124       ware   Foundation,  Inc.,  59  Temple  Place,  Suite  330,  Boston,  MA
125       02111-1307 USA
126
127       The original copyright holder can be contacted via email or as
128
129       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
130       buehlplatz 41 70178 Stuttgart Germany
131
132
133
134epclextract 2.5-DEBUG            January 2021                   EPCLEXTRACT(1)
Impressum