NAME
pcs - checks SPASS proofs
SYNOPSIS
pcs [ -cdfrstv] file
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
Assumptions \wedge \neg Conclusion
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.
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.
SEE ALSO
checkstat(1), filestat(1), pgen(1), rescmp(1), tpform(1), tpget(1),
deprose(1), dfg2otter(1), dfg2otterpl(1), SPASS(1)
AUTHORS
Thorsten Engel and Christian Theobalt.
Contact : Thomas Hillenbrand <hillen@mpi-sb.mpg.de>
Christoph Weidenbach <weidenb@mpi-sb.mpg.de>