checkproof

CHECKPROOF(1)                    User Commands                   CHECKPROOF(1)



NAME
       checkproof - manual page for checkproof 1.9

SYNOPSIS
       checkproof [options] [files]

DESCRIPTION
       checkproof 1.9

       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
       believe 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
       verify 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
              output. 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.
              Determines 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
              syntax 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
              executable 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-2014 by Stephan Schulz, schulz@eprover.org

       This program is a part of the support structure for the E equational
       theorem prover. 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
       MERCHANTABILITY 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
       Software Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA
       02111-1307 USA

       The original copyright holder can be contacted as

       Stephan Schulz DHBW Stuttgart Fakultaet Technik Informatik
       Rotebuehlplatz 41 70178 Stuttgart Germany



checkproof 1.9                     July 2015                     CHECKPROOF(1)