LP, the Larch Prover -- Subgoals


A subgoal is a conjecture introduced by a method of backward inference in an attempt to prove another conjecture. Often additional hypotheses may be used in the proof of the subgoal.