LP, the Larch Prover -- Assigning names to facts

Each fact in LP's logical system has a name consisting of an alphanumeric prefix followed by a series of numeric suffixes separated by periods.

Syntax

<name>      ::= <simpleId> <extension>*
<extension> ::= . <number>

Examples

arith.1
set.2.3

Usage

LP assigns new names to facts in response to the assert and fix commands, to critical pair equations in response to the critical-pairs and complete commands, and to conjectures in response to the prove command. These names have a single numeric <extension>, whose value increases each time a new name is required. Users can specify the name prefix for a fact in the assert command, or for a conjecture in the prove command, by writing :<simpleId>: before the fact. Otherwise the value of the name-prefix setting governs the <simpleId> used as a prefix for new names.

Normalization, ordering, unordering, and proofs preserve the names of formulas, rewrite rules, and deduction rules. LP assigns subnames (i.e., names with an additional <extension>) to instantiations of formulas, rewrite rules, and deduction rules, to the results of applying deduction rules, and to hypotheses introduced during the proof of a conjecture. The names of the results of applying a deduction rule to a formula extend the name of the deduction rule if the deduction rule has more than one hypothesis; otherwise they extend the name of the formula.

One fact is called a descendant of another (and the latter is called an ancestor of the former) if the name of the first extends, by zero or more <extension>s, the name of the second. A proper ancestor (or descendant) of a fact is an ancestor (or descendant) with a different name.

The names of the hardwired deduction rules for formulas begin with lp_. The hardwired rewrite rules for the logical connectives, the conditional and equality operators, and the quantifiers do not have names, nor do conjectures introduced as subgoals in proofs.

See also