**proof.sty:
A User Guide**

**3. Chaining uses of the rules to build proofs**

Suppose we want to set this derivation of one of De Morgan's Laws:

Proceed from the bottom up. So we start

\infer[^{(2)}] {\neg(\phi \land \psi} {\bot} |

Note the use of superscript to generate a small label. Now replace '\bot' with the inference of which it is the conclusion:

\infer[^{(2)}] |

Don't worry about the spacing of the top premiss list. It will automatically adjust as the proof-tree is extended upward. Now again replace the first '\bot' in the premiss-list with the inference of which it is the conclusion:

\infer[^{(2)}] |

To put a 'premiss discharge' rule over the negated phi, treat that as an inference from the null list of premisses:

\infer[^{(2)}] |

And keep on going in the same way!

Obvious tip: It goes without saying that it is only too easy to lose a vital bracket. So set proofs incrementally as just illustrated, and LaTeX them to check the output every couple of steps (and put the proof initially in a short separate file so you can check the output speedily).

**4. Further tricks and tips **(next
page)

Previous page of this mini-guide | Back to proofs page | Home