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

FreeBSD Manual Pages


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

       checkproof - manual page	for checkproof 2.0

       checkproof [options] [files]

       checkproof 2.0

       Read  an	UPCL2 protocol and verify the inferences using one of a	varity
       of external provers.

       This is a _very_	experimental program. Passing checkproof does indicate
       that  all  inferences  in  an UPCL2 protocol are	correct	(i.e. that the
       conclusion is logically implied by the premisses) - that	is, if you be-
       lieve  that the transformation process and the used prover are correct.
       However,	checkproof will	e.g. gladly show that the empty	proof protocol
       does not	contain	any buggy steps.

       If  a  proof  protocol  fails to	pass this test,	the proof may still be
       correct.	Due to e.g. incomplete strategies (this	applies	in  particular
       to Otter), build-in limits (Otter), and bugs in the prover (potentially
       all systems, but	observed in SPASS 0.55), a prover might	fail to	verify
       a correct step. Moreover, due to	the different strategies, calculi, and
       in particular different term orderings chosen by	the systems, a	single
       UPCL2 inference may result in a proof problem that is very hard to ver-
       ify for other provers. However, if a proof step	is  rejected  by  more
       than one	system,	you should probably look at this step in detail.




	      Print a short description	of program usage and options.


	      Print the	version	number of the program.



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

       -o <arg>


	      Redirect output into the named file.



	      Equivalent to --output-level=0.

       -l <arg>


	      Select  an  output level,	greater	values imply more verbose out-
	      put. At the moment, level	0 only	prints	the  result,  level  1
	      prints  inference	 steps	as  they  are verified,	level 2	prints
	      prover commands issued, and level	3  prints  all	prover	output
	      (which may be very little)

       -p <arg>


	      Set the type of the prover to use	for proof verification.	Deter-
	      mines problem syntax, options, and check for success.  Supported
	      options	at   are   'E'	 (the  default),'Otter'	 'SPASS',  and
	      'scheme-setheo' (not yet implemented).  SPASS  support  is  only
	      tested  with  SPASS  0.55	 and  may fail if the problem contains
	      identifiers reserved by SPASS. There have	been some supple  syn-
	      tax changes, so more recent SPASS	versions will probably fail as

       -x <arg>


	      Give the name under which	the prover can be called. If  no  exe-
	      cutable is given,	checkproof will	guess a	name based on the type
	      of the prover. This guess	may be way off!

       -t <arg>


	      Limit the	CPU time prover	may spend on a single step. Default is
	      10 seconds.

       Report  bugs  to	<>. Please include the following, if

       * 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 1998-2017 by Stephan Schulz,,  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

       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-
       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

checkproof 2.0			  August 2020			 CHECKPROOF(1)


Want to link to this manual page? Use this URL:

home | help