home | help
EPCLEXTRACT(1)			  User Commands 		  EPCLEXTRACT(1)

NAME
     epclextract - manual page for epclextract 2.6

SYNOPSIS
     epclextract [options] [files]

DESCRIPTION
     epclextract 2.6

     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  --ver-
	    bose=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 con-
	    vert 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  pos-
     sible:

     * 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-2021  by Stephan Schulz, schulz@eprover.org, and the E con-
     tributors (see DOC/CONTRIBUTORS).

     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  addi-
     tional information at http://www.eprover.org

     This program is free software; you can redistribute it and/or modify it un-
     der  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 FIT-
     NESS 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 Foun-
     dation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307 USA

     The original copyright holder can be contacted via email or as

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

epclextract 2.6 		   August 2026			  EPCLEXTRACT(1)

home | help