LP, the Larch Prover  Sample proofs: useful kinds of axioms
The axioms in set1.lp fall into several categories:
 Induction rules

The first axiom, sort Set generated by {}, insert, asserts that all
elements of sort S can be obtained by finitely many applications of
insert to {}. It provides the basis for definitions and proofs by
induction.
 Explicit definitions

The second axiom, {e} = insert(e, {}), is a single formula
that defines the operator {__} (as a constructor for a singleton set).
 Inductive definitions

The next two pairs of axioms provide induction definitions of the membership
operator \in and the subset operator \subseteq. Inductive definitions
generally consist of one formula per generator.
 Implicit definitions

The final formula, e \in (x \union y) <=> e \in x \/ e \in y, in the first
assert command, together with the other axioms, completely constrains the
interpretation of the \union operator.
 Constraining properties

The second assert command formalizes the
principle of extensionality, which asserts that any two sets with exactly
the same elements must be the same set.