[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4. pcs


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4.1 NAME

pcs - checks SPASS proofs


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4.2 SYNOPSIS

pcs [ -cdfrstv] file


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4.3 DESCRIPTION

pcs is a Perl script that supports automatic checking of proofs specified in DFG syntax with the theorem prover OTTER. It uses pcs checks that: The second condition is verified by checking the unsatisfiability
for each proof step (inference rule application) by running OTTER for a limited time. The appropriate DFG files for these problems are generated by pgen. OTTER may fail to terminate within this time, leaving the correctness of a proof step undecided, which leads to the three possible results of pcs:

pcs uses a working directory, in which all proof tasks corresponding to the proof steps are generated using the pgen program. These tasks are subsequently checked using OTTER.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4.4 OPTIONS

Several options control the behavior of pcs when it fails to verify a proof step, its output and the naming of generated files and the working directory:

-c
Continue even if a single proof step could not be verified. Default 'off'.
-d suffix
Suffix of created working directory. For an input file root.ext, the working directory <root><suffix> is created. If suffix does not end with a backslash, it is taken as a prefix for files generated by pgen, which are then created in the current working directory. Default is '_SubProofs/'.
-f
Overwrite working directory if it already exists. Default 'off'.
-o
Use SPASS as proof checker instead of OTTER. This option is especially useful when checking proofs generated by a different prover. Default is 'off'.
-p path
Location of DFG prover to be used instead of the default one. If -o is specified, then it overrides this option, and SPASS is used instead. If a DFG converter is specified, then a prover must be specified as well. Default is OTTER.
-q
Be quiet and do not print program paths. This option is especially useful inside checkstat. Default is 'off'.
-r
Clean up all generated files at the end, even if the proof is not valid. Default 'off'.
-s suffix
Suffix of files generated by pgen. Default is '.dfg'.
-t limit
Number of seconds for each proof attempt for each proof step. Default is 3 seconds.
-v
(verbose) Give some progress information. Default is 'off'.
-w path
Location of DFG converter to be used instead of the default one. If a DFG converter is specified, then a prover must be specified as well. Default is dfg2otter.pl.


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4.5 AUTHORS

Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>


[ < ] [ > ]   [ << ] [ Up ] [ >> ]         [Top] [Contents] [Index] [ ? ]

4.6 SEE ALSO

checkstat(1), filestat(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)


[ << ] [ >> ]           [Top] [Contents] [Index] [ ? ]

This document was generated by Renate Schmidt on March, 10 2003 using texi2html