Ubuntu Manpage: epclextract - manual page for epclextract 3.2.5

NAME

       epclextract - manual page for epclextract 3.2.5

SYNOPSIS

       epclextract [options] [files]

DESCRIPTION

       epclextract 3.2.5

       Read  an  PCL2  protocol and print the steps necessary for proving the clauses in "proof",
       "final", or "extract" steps.

       Options

       -h

       --help

              Print a short description of program usage and options.

       -V

       --version

              Print the version number of the program.

       -v

       --verbose[=<arg>]

              Verbose comments on the progress of the program. The short form or  the  long  form
              without the optional argument is equivalent to --verbose=1.

       -f

       --fast-extract

              Do  a  fast  extract. With this option the program understands only a subset of PCL
              and assumes that all "proof" and "final" steps are at the end of the protocoll.

       -C

       --forward-comments

              Pass comments found in the input through to the output while reading input.

       -c

       --competition-framing

              Print special "begin" and "end"comments around the proof object, as required by the
              CASC MIX* class.

       -n

       --no-extract

              Don't extract, print back all steps (actually, it treats all steps as proof steps).
              Useful as a syntax checker, or if you want to convert PCL to  TSTP  with  the  next
              option.

       --tstp-out

              Print proof protocol in TSTP syntax (default is PCL).

       --tptp3-out

              Synonymous with --tstp-out.

       -o <arg>

       --output-file=<arg>

              Redirect output into the named file.

       -s

       --silent

              Equivalent to --output-level=0.

REPORTING BUGS

       Report bugs to <schulz@eprover.org>. Please include the following, if possible:

       * 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 happened.

       * If possible all input files necessary to reproduce the bug.

COPYRIGHT

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
http://www.eprover.org

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 MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
See the GNU General 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 Software Foundation, Inc., 59 Temple Place, Suite 330,
Boston, MA 02111-1307 USA

We welcome bug reports and even reasonable questions. If the prover behaves in an
unexpected way, please include the following information:

- What did you observe? - What did you expect? - The output of `eprover --version` - The
full commandline that lead to the unexpected behaviour - The input file(s) that lead to
the unexpected behaviour

Most bug reports should be send to <schulz@eprover.org>. Bug reports with respect to the
HO-version should be send to or at least copied to <jasmin.blanchette@gmail.com>. Please
remember that this is an unpaid volunteer service.

The original copyright holder can be contacted via email or as

Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Lerchenstrasse 1 70174
Stuttgart Germany