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>