Next: Conditional proofs
Up: Proof semantics
Previous: Rules dealing with equality
  Contents
Composite proofs
Composite proofs are used to link together multiple inference steps
in such a way that the conclusions of earlier deductions become
available in subsequent deductions. Specifically, to evaluate a
composite proof
in some assumption base
, we first evaluate
in
, obtaining some conclusion
; and we then evaluate
in the augmented assumption base
.
This means that the conclusion of
becomes available (serves as a ``lemma'')
inside
. The conclusion
we obtain by evaluating
in
becomes the
conclusion of the entire composition
. This is formally
specified as follows:
2004-08-04