= Proof goal transformation
Reading an <inference rule> backwards to replace a desired conclusion by sufficient subgoals. A conjunction goal can be replaced by its two conjuncts using the <conjunction introduction rule>; an available disjunction can instead lead to two case subgoals using the <disjunction elimination rule>. Different choices change the organization and sharing of <subproofs>. Scope and <assumption discharge> conditions remain obligations even when a rule is applied backwards during proof search.
Back to article page
