LP, the Larch Prover -- The complete command

The complete command provides a method of forward inference that extends the critical-pairs command.

Syntax

<complete-command> ::= complete

Examples

complete

Usage

The complete command enlarges LP's logical system by adding consequences of facts already in the system. It operates by computing critical pair equations between rewrite rules in the system, orienting them into new rewrite rules, and iterating this procedure until there are no further nontrivial critical pair equations.

When LP's logical system consists solely of active, nonimmune, quantifier-free equations and rewrite rules, the complete command attempts to transform the logical system into a convergent set of rewrite rules that has the same equational theory. The completion procedure is based on the Peterson and Stickle extension of the Knuth-Bendix completion procedure.

LP terminates the completion procedure if the current conjecture reduces to true.

A convergent rewriting system can be used to prove theorems by normalization using the prove command or to reduce terms to a canonical form using the show normal-form command. The completion-mode setting controls the operation of the completion procedure. You can interrupt and resume the operation of the completion procedure.