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.