LP, the Larch Prover -- Operational syntax and semantics
The basis for each proof in LP is a logical system that contains a collection
of facts (axioms, hypotheses, and previously proved theorems) available for use
in that proof. There is a separate logical system, known as a proof context,
for the proof of each conjecture and subgoal.
The facts in a logical system have both semantic content (expressed by formulas
in first-order logic) and operational content. For more information about this
operational content, see: