---
name: "pcs"
section: "1"
platform: "linux"
package: "spass"
version: "2.1-4"
release: "Debian 5.0 (Lenny)"
platforms: ["linux"]
url: "https://new.carta.tech/pcs"
---

# pcs(1)

checks SPASS proofs

## 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)](/pgen/1.md), *rescmp*(1), *tpform*(1), *tpget*(1), *deprose*(1), [*dfg2otter*(1)](/dfg2otter/1.md), *dfg2otterpl*(1), [*SPASS*(1)](/SPASS/1.md)

## AUTHORS

Thorsten Engel and Christian Theobalt.

Contact : Thomas Hillenbrand \<hillen@mpi-sb.mpg.de\>\
           Christoph Weidenbach \<weidenb@mpi-sb.mpg.de\>