LP, the Larch Prover — The assert command

The assert command adds axioms to LP's logical system.

Syntax

<assert-command> ::= assert <assertion>;+ [;]
<assertion>      ::= [:<simpleId>:] <fact>
<fact>           ::= <formula> | <deduction-rule> | <induction-rule> 
                        | <operator-theory> | <partitioned-by>

Examples

assert
  e1 \in insert(e2, s) <=> e1 = e2 \/ e1 \in s;
  when \A e (e \in s1 <=> e \in s2) yield s1 = s2;
  Set generated by {}, insert;
  ac \U;
  Set partitioned by \in
  ..

Usage

LP adds the asserted facts to its logical system. It assigns a name to each of these facts using the current name-prefix setting, unless an assertion begins with :<simpleId>:, in which case LP uses that identifier as the name-prefix for that assertion.

LP takes certain default actions when it adds assertions to its logical system.

It translates <partitioned-by>s into deduction rules.
It normalizes asserted formulas and deduction rules (unless the immunity setting dictates otherwise).
It attempts to orient asserted formulas into terminating rewrite rules (unless the automatic-ordering setting dictates otherwise).
It uses new rewrite rules to normalize the other formulas and deduction rules (unless the activity setting dictates otherwise).
It uses new deduction rules to deduce consequences from formulas and rewrite rules (again, unless the activity setting dictates otherwise).
It registers operators asserted to be ac or commutative as having multiset status. If any of these operators had a non-ac (or noncommutative) polynomial interpretation, LP prints a warning and gives the operator a default ac (or commutative) polynomial interpretation.
It turns all rewrite rules containing an operator asserted to be ac or commutative back into formulas, and it reflattens all facts containing these operators. This process can change these facts or even reduce them to true, as is the case for the commutativity equation.