LP, the Larch Prover -- Logical syntax and semantics

LP is a proof assistant for multisorted first-order logic. Except for the fact that it provides a rich set of notations for functions, LP is based on the syntax and semantics for first-order logic found in many textbooks. For a description of this syntax and semantics, see:

Conventions for describing LP's syntax
Symbols
Sorts
Variables
Operators
Quantifiers
Terms
Formulas