FreeBSD Manual Pages
CHECKPROOF(1) User Commands CHECKPROOF(1) NAME checkproof - manual page for checkproof 2.6 SYNOPSIS checkproof [options] [files] DESCRIPTION checkproof 2.6 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-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 checkproof 2.6 November 2025 CHECKPROOF(1)
NAME | SYNOPSIS | DESCRIPTION | REPORTING BUGS | COPYRIGHT
Want to link to this manual page? Use this URL:
<https://man.freebsd.org/cgi/man.cgi?query=checkproof&sektion=1&manpath=FreeBSD+Ports+15.0>