<name> ::= <simpleId> <extension>* <extension> ::= . <number>
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.