next up previous contents
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 $D_1;D_2$ in some assumption base $\beta$, we first evaluate $D_1$ in $\beta$, obtaining some conclusion $F_1$; and we then evaluate $D_2$ in the augmented assumption base $\mbox{$\beta$}\cup \{F_1\}$. This means that the conclusion of $D_1$ becomes available (serves as a ``lemma'') inside $D_2$. The conclusion we obtain by evaluating $D_2$ in $\mbox{$\beta$}\cup \{F_1\}$ becomes the conclusion of the entire composition $D_1;D_2$. This is formally specified as follows:
$\;\;$ $\mbox{$\beta$}\mbox{$\:\vdash\:$}D_1 \mbox{$\:\longrightarrow\;$}F_1 \;\;\;\;\; \mbox{$\beta$}\cup \{F_1\} \mbox{$\:\vdash\:$}D_2 \mbox{$\:\longrightarrow\;$}F_2$$\;$  
  $\;\:$
$\;\;$ $\mbox{$\beta$}\mbox{$\:\vdash\:$}D_1;D_2 \mbox{$\:\longrightarrow\;$}F_2$$\;$  


2004-08-04