1CHECKPROOF(1) User Commands CHECKPROOF(1)
2
6 checkproof - manual page for checkproof 2.6-DEBUG
7
9 checkproof [options] [files]
10
12 checkproof 2.6-DEBUG
13 Read an UPCL2 protocol and verify the inferences using one of a varity
15 of external provers.
16 This is a _very_ experimental program. Passing checkproof does indicate
18 that all inferences in an UPCL2 protocol are correct (i.e. that the
19 conclusion is logically implied by the premisses) - that is, if you be‐
20 lieve that the transformation process and the used prover are correct.
21 However, checkproof will e.g. gladly show that the empty proof protocol
22 does not contain any buggy steps.
23 If a proof protocol fails to pass this test, the proof may still be
25 correct. Due to e.g. incomplete strategies (this applies in particular
26 to Otter), build-in limits (Otter), and bugs in the prover (potentially
27 all systems, but observed in SPASS 0.55), a prover might fail to verify
28 a correct step. Moreover, due to the different strategies, calculi, and
29 in particular different term orderings chosen by the systems, a single
30 UPCL2 inference may result in a proof problem that is very hard to ver‐
31 ify for other provers. However, if a proof step is rejected by more
32 than one system, you should probably look at this step in detail.
33 Options
35 -h
37 --help
39 Print a short description of program usage and options.
41 --version
43 Print the version number of the program.
45 -v
47 --verbose[=<arg>]
49 Verbose comments on the progress of the program. The short form
51 or the long form without the optional argument is equivalent to
52 --verbose=1.
53 -o <arg>
55 --output-file=<arg>
57 Redirect output into the named file.
59 -s
61 --silent
63 Equivalent to --output-level=0.
65 -l <arg>
67 --output-level=<arg>
69 Select an output level, greater values imply more verbose out‐
71 put. At the moment, level 0 only prints the result, level 1
72 prints inference steps as they are verified, level 2 prints
73 prover commands issued, and level 3 prints all prover output
74 (which may be very little)
75 -p <arg>
77 --prover-type=<arg>
79 Set the type of the prover to use for proof verification. Deter‐
81 mines problem syntax, options, and check for success. Supported
82 options at are 'E' (the default),'Otter' 'SPASS', and
83 'scheme-setheo' (not yet implemented). SPASS support is only
84 tested with SPASS 0.55 and may fail if the problem contains
85 identifiers reserved by SPASS. There have been some supple syn‐
86 tax changes, so more recent SPASS versions will probably fail as
87 well.
88 -x <arg>
90 --executable=<arg>
92 Give the name under which the prover can be called. If no exe‐
94 cutable is given, checkproof will guess a name based on the type
95 of the prover. This guess may be way off!
96 -t <arg>
98 --prover-cpu-limit=<arg>
100 Limit the CPU time prover may spend on a single step. Default is
102 10 seconds.
103
105 Report bugs to <schulz@eprover.org>. Please include the following, if
106 possible:
107 * The version of the package as reported by eprover --version.
109 * The operating system and version.
111 * The exact command line that leads to the unexpected behaviour.
113 * A description of what you expected and what actually happend.
115 * If possible all input files necessary to reproduce the bug.
117
119 Copyright 1998-2021 by Stephan Schulz, schulz@eprover.org, and the E
120 contributors (see DOC/CONTRIBUTORS).
121 This program is a part of the distribution of the equational theorem
123 prover E. You can find the latest version of the E distribution as well
124 as additional information at http://www.eprover.org
125 This program is free software; you can redistribute it and/or modify it
127 under the terms of the GNU General Public License as published by the
128 Free Software Foundation; either version 2 of the License, or (at your
129 option) any later version.
130 This program is distributed in the hope that it will be useful, but
132 WITHOUT ANY WARRANTY; without even the implied warranty of MER‐
133 CHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General
134 Public License for more details.
135 You should have received a copy of the GNU General Public License along
137 with this program (it should be contained in the top level directory of
138 the distribution in the file COPYING); if not, write to the Free Soft‐
139 ware Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
140 02111-1307 USA
141 The original copyright holder can be contacted via email or as
143 Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik Rote‐
145 buehlplatz 41 70178 Stuttgart Germany
146checkproof 2.6-DEBUG July 2021 CHECKPROOF(1)