The PCS Prover

Main Idea of the PCS Prover

The PCS proof method (BB 2000) aims at generating "natural" proofs.

Roughly, the PCS prover proceeds by iteratively going through the following three phases:

The P-phase ("Proving" phase)

The C-phase ("Computing" phase)

The S-phase ("Solving" phase)

It reduces proving of formulae with "alternating quantifiers" to solving.

A Proof Generated by the PCS Prover

                         show