LP, the Larch Prover -- The show command

The show command displays the results of certain operations without affecting the state of LP's logical system.

Syntax

<show-command> ::= show normal-form <term>
                      | show unifiers  <term>,  <term>

Note: The first argument of the show command can be abbreviated.

Examples

show n-f e \in (s \U s)
show unifiers e*x, i(y)*y

Usage

The show normal-form command displays a normal form of the term with respect to the currently active rewrite rules. If the trace-level is nonzero, LP also displays successive reductions of the term leading to the normal form.

The show unifiers command displays a complete set of most general unifiers of two terms. It displays the unifying substitutions along with the unifications of the terms, and it uses unification algorithms appropriate to the theories associated with the operators in the terms.