LP, the Larch Prover -- Proofs of deduction rules

LP permits users to prove deduction rules as well as assert them. It automatically generates a single subgoal when asked to initiate a proof of a deduction rule. The subgoal involves showing that the conjunction of the hypotheses of the deduction rule implies the conjunction of its conclusions.

For example, the command

prove when \A x:Elem (x \in s:Set <=> x \in t:Set) yield s = t

causes LP to generate a single subgoal which involves proving the formula

\A x:Elem (x \in s:Set <=> x \in t:Set) => s = t

LP also generates a single subgoal when asked to initiate a proof of a partitioned-by. This subgoal is the one associated with the translation of the partitioned-by into a deduction rule.