Pc-Nqthm, An interactive ``Proof-checker'' enhancement
of the Boyer-Moore Theorem Prover

The Logic

The Proof Checker

This proof-checker is loaded on top of the Boyer-Moore Theorem Prover; see the Theorem Prover section in the Nqthm description.

The user can give commands at a low level (such as deleting a hypothesis, diving to a subterm of the current term, expanding a function call, or applying a rewrite rule) or at a high level (such as invoking the Boyer-Moore Theorem Prover). Commands also exist for displaying useful information (such as printing the current hypotheses and conclusion, displaying the currently applicable rewrite rules, or showing the current abbreviations) and for controlling the progress of the proof (such as undoing a specified number of commands, changing goals, or disabling certain rewrite rules). A notion of ``macro commands'' lets the user create compound commands, roughly in the spirit of the tactics and tacticals of LCF and its descendents. An on-line help facility is provided, and a user's manual exists.

As with a variety of proof-checking systems, this system is goal-directed: a proof is completed when the main goal and all subgoals have been proved. Upon completion of an interactive proof, the lemma with its proof may be stored as a Boyer-Moore `event' that can be added to the user's current library of definitions and lemmas. This event can later be replayed in `batch mode'. Partial proofs can also be stored.

Accomplishments

This system has been used to check theorems stating the correctness of a transitive closure program, a Towers of Hanoi program, a ground resolution prover, a compiler, irrationality of the square root of 2, an algorithm of Gries for finding the largest "true square" submatrix of a boolean matrix, the exponent two version of Ramsey's Theorem, the Shroeder-Bernstein theorem, Koenig's tree lemma, and others. It has also been used to check the correctness of several Unity programs and has been used for hardware verification.

Published articles and reports

The first one below is a detailed user's manual, including soundness arguments. The second extends this by describing an extension of the system which admits free variables, an important addition for doing full first-order reasoning. The third is a reference for that full first-order reasoning capability.

Matt Kaufmann, A User's Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover. Technical Report 19, Computational Logic, Inc., May, 1988.

Matt Kaufmann, Addition of Free Variables to an Interactive Enhancement of the Boyer-Moore Theorem Prover. Technical Report 42, Computational Logic, Inc., May, 1989.

Matt Kaufmann, An Extension of the Boyer-Moore Theorem Prover to Support First-Order Quantification. To appear in J. of Automated Reasoning. A preliminary (and expanded) version appears as Technical Report 43, Computational Logic, Inc., May, 1989.

Strengths/weaknesses/suitability:

Strengths include:

Combination of capability for high degree of user control with the power of the Boyer-Moore prover
On-line help facility and users manuals
Extensibility by way of ``macro commands'' (patterned after the tactics and tacticals of LCF, HOL, Nuprl etc.)
Full integration into Boyer-Moore system
Careful attention to soundness issues

Weaknesses include:

Ease of low-level interaction often tempts users to construct ugly proofs without many reusable lemmas that are hard to modify.
First-order quantification is handled via Skolemization, rather than directly (as in the Never prover).

To obtain PC-Nqthm.