LP, the Larch Prover -- The assert command

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


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


  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


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.