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: