Skip site navigation (1)Skip section navigation (2)

FreeBSD Manual Pages

  
 
  

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
	      --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-2021  by	 Stephan Schulz, schulz@eprover.org, and the E
       contributors (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 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  MER-
       CHANTABILITY  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	 Soft-
       ware   Foundation,  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	 Rote-
       buehlplatz 41 70178 Stuttgart Germany

epclextract 2.6			 November 2025			EPCLEXTRACT(1)

Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=epclextract&sektion=1&manpath=FreeBSD+Ports+15.0>

home | help