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

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.

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 and Christian Theobalt.

Contact : spass@mpi-inf.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 Christoph Weidenbach on February, 23 2010 using texi2html 1.78.