epclextract

EPCLEXTRACT(1)                   User Commands                  EPCLEXTRACT(1)



NAME
       epclextract - manual page for epclextract 1.9

SYNOPSIS
       epclextract [options] [files]

DESCRIPTION
       epclextract 1.9

       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 requiered 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 happend.

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

COPYRIGHT
       Copyright 1998-2014 by Stephan Schulz, schulz@eprover.org

       This program is a part of the support structure for the E equational
       theorem prover. 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

       The original copyright holder can be contacted as

       Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
       Rotebuehlplatz 41 70178 Stuttgart Germany



epclextract 1.9                    July 2015                    EPCLEXTRACT(1)