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

FreeBSD Manual Pages

  
 
  

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

NAME
       checkproof - manual page	for checkproof 2.0

SYNOPSIS
       checkproof [options] [files]

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

       Options

       -h

       --help

	      Print a short description	of program usage and options.

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

       -o <arg>

       --output-file=<arg>

	      Redirect output into the named file.

       -s

       --silent

	      Equivalent to --output-level=0.

       -l <arg>

       --output-level=<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>

       --prover-type=<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
	      well.

       -x <arg>

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

       --prover-cpu-limit=<arg>

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

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

checkproof 2.0			  August 2020			 CHECKPROOF(1)

NAME | SYNOPSIS | DESCRIPTION | REPORTING BUGS | COPYRIGHT

Want to link to this manual page? Use this URL:
<https://www.freebsd.org/cgi/man.cgi?query=checkproof&sektion=1&manpath=FreeBSD+12.2-RELEASE+and+Ports>

home | help