Paul Taylor's Proof Trees, 17 August 1990 %% Build proof tree for Natural Deduction, Sequent Calculus, etc. %% WITH SHORTENING OF PROOF RULES! %% Paul Taylor, begun 10 Oct 1989 %% *** THIS IS ONLY A PRELIMINARY VERSION AND THINGS MAY CHANGE! *** %% %% \prooftree %% hyp1 produces: %% hyp2 %% hyp3 hyp1 hyp2 hyp3 %% \justifies -------------------- rulename %% concl concl %% \thickness=0.08em %% \shiftright 2em %% \using %% rulename %% \endprooftree %% %% where the hypotheses may be similar structures or just formulae. %% %% To get a vertical string of dots instead of the proof rule, do %% %% \prooftree which produces: %% [hyp] %% \using [hyp] %% name . %% \proofdotseparation=1.2ex .name %% \proofdotnumber=4 . %% \leadsto . %% concl concl %% \endprooftree %% %% Within a prooftree, $and$ may be used instead of \prooftree and %% \endprooftree; this is not permitted at the outer level because it %% conflicts with LaTeX. Also, %% \Justifies %% produces a double line. In LaTeX you can use \begin{prooftree} and %% \end{prootree} at the outer level (however this will not work for the inner %% levels, but in any case why would you want to be so verbose?). %% %% All of of the keywords except \prooftree and \endprooftree are optional %% and may appear in any order. They may also be combined in \newcommand's %% eg "\def\Cut{\using\sf cut\thickness.08em\justifies}" with the abbreviation %% "\prooftree hyp1 hyp2 \Cut \concl \endprooftree". This is recommended and %% some standard abbreviations will be found at the end of this file. %% %% \thickness specifies the breadth of the rule in any units, although %% font-relative units such as "ex" or "em" are preferable. %% It may optionally be followed by "=". %% \proofrulebreadth=.08em or \setlength\proofrulebreadth{.08em} may also be %% used either in place of \thickness or globally; the default is 0.04em. %% \proofdotseparation and \proofdotnumber control the size of the %% string of dots %% %% If proof trees and formulae are mixed, some explicit spacing is needed, %% but don't put anything to the left of the left-most (or the right of %% the right-most) hypothesis, or put it in braces, because this will cause %% the indentation to be lost. %% %% By default the conclusion is centered wrt the left-most and right-most %% immediate hypotheses (not their proofs); \shiftright or \shiftleft moves %% it relative to this position. (Not sure about this specification or how %% it should affect spreading of proof tree.)