4. pcs
4.1 NAME
pcs - checks SPASS proofs
4.2 SYNOPSIS
pcs [ -cdfrstv] file
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
-
the C-program pgen, which generates proof tasks corresponding to inference steps for each proof step of a DFG proof and checks the tableau structure.
-
the C-program SPASS with the -Flotter option for converting
DFG syntax files with formulas into DFG syntax files with
clauses.
-
the C-program dfg2otter, which transforms files in DFG syntax with
clauses only into files for OTTER syntax.
pcs checks that:
-
The conclusion in each proof step is a logical consequence
of the assumptions in that proof step.
-
Each clause in a subtableau uses only parents clauses that are
visible at this point in the tableau.
-
Each clause, except for split clauses, has the maximum
split level of its parents.
-
If the first half of a split was ground, then negations
of its literals can be used in the tableau branch corresponding
to the second half of the split.
-
The tableau is complete and closed.
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:
-
The proof is correct: Both conditions are satisfied for all proof steps.
-
The proof is not correct: One condition is definitely violated for
at least one proof step.
-
Correctness is undecided: The first condition is satisfied,
but the second condition could not be verified nor falsified for at least
one proof step.
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.
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.
4.5 AUTHORS
Thorsten Engel
Christian Theobalt
Contact : Christoph Weidenbach <weidenb@mpi-sb.mpg.de>
4.6 SEE ALSO
checkstat(1), filestat(1), pgen(1), rescmp(1), tpform(1), tpget(1), deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
This document was generated
by Renate Schmidt on March, 10 2003
using texi2html