1CHECKPROOF(1)                    User Commands                   CHECKPROOF(1)
2
3
4

NAME

6       checkproof - manual page for checkproof 2.6-DEBUG
7

SYNOPSIS

9       checkproof [options] [files]
10

DESCRIPTION

12       checkproof 2.6-DEBUG
13
14       Read  an UPCL2 protocol and verify the inferences using one of a varity
15       of external provers.
16
17       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
24       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
34       Options
35
36       -h
37
38       --help
39
40              Print a short description of program usage and options.
41
42       --version
43
44              Print the version number of the program.
45
46       -v
47
48       --verbose[=<arg>]
49
50              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
54       -o <arg>
55
56       --output-file=<arg>
57
58              Redirect output into the named file.
59
60       -s
61
62       --silent
63
64              Equivalent to --output-level=0.
65
66       -l <arg>
67
68       --output-level=<arg>
69
70              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
76       -p <arg>
77
78       --prover-type=<arg>
79
80              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
89       -x <arg>
90
91       --executable=<arg>
92
93              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
97       -t <arg>
98
99       --prover-cpu-limit=<arg>
100
101              Limit the CPU time prover may spend on a single step. Default is
102              10 seconds.
103

REPORTING BUGS

105       Report  bugs  to <schulz@eprover.org>. Please include the following, if
106       possible:
107
108       * The version of the package as reported by eprover --version.
109
110       * The operating system and version.
111
112       * The exact command line that leads to the unexpected behaviour.
113
114       * A description of what you expected and what actually happend.
115
116       * 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
122       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
126       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
131       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
136       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
142       The original copyright holder can be contacted via email or as
143
144       Stephan  Schulz  DHBW  Stuttgart  Fakultaet  Technik  Informatik  Rote‐
145       buehlplatz 41 70178 Stuttgart Germany
146
147
148
149checkproof 2.6-DEBUG             January 2023                    CHECKPROOF(1)
Impressum