These macros are meant to provide the ability to construct tree derivations (for example, type derivations or logical proofs) in an easy and flexible way. They are built on top of the excellent prooftree macros by Paul Taylor, and are a refinement of some macros written by Steffen van Bakel, from whom I learned how to do this stuff. Jayshan Raghunandan has also contributed by spotting and fixing a couple of bugs in the original definition.

Although there are lots of auxiliary definitions, the only one you need to manually use is \Inf

It creates inference rules (in math mode) with as many premises as you like, and an optional rule name (which is shown in brackets to the right of the rule) and optional further superscript text to go after the brackets around the rule name (which I use for asterisks or footnotes about side-conditions).

You use it (for n>=0) as follows:

For a rule with no name: \Inf{premise_1}{premise_2}…{premise_n}{conclusion}

For a rule with a name: \Inf[rulename]{premise_1}{premise_2}…{premise_n}{conclusion}

For example, \Inf[name]{a}{b}{c} produces something like

  a   b
---------(name)
c

For a rule with a name and with some text to be placed superscript after the brackets (e.g., for providing side-conditions as footnotes underneath): \Inf[rulename][superscript_text]{premise_1}{premise_2}…{premise_n}{conclusion}

Finally, there is a feature which works nicely if you're defining rules with many premises : you can insert a . in between arguments, to start a new line of premises. For example,

\Inf[name]{p1}{p2}{p3}.{p4}{p5}{c}

produces something like

 p1  p2  p3
p4    p5
------------(name)
c

Here are the macros (stick the stuff below near the top of your file), which have been very mildly tested in their present form, but I believe are ok. You can nest \Inf calls in premises to your heart's content, and much further still. I have no idea what happens if you nest them in conclusions, or even in premises if you choose to have multiple lines of premises..

\usepackage{prooftree}

\makeatletter

\newskip \point

\point =1pt

\def \RulePremisesNewlineMore[#1]#2.#3#4{\@ifnextchar\bgroup{\RulePremisesNewlineMore[#1]{#2}.{#3\premisespacing#4}}{\@ifnextchar.{\RulePremisesNewline[#1]{{\begin{array}{c}#2\\#3\premisespacing#4\end{array}}}}{\RuleMultiPremise[#1]{{\begin{array}{c}#2\\#3\end{array}}}{#4}}}}

\def \RulePremisesNewline[#1]#2.#3{\@ifnextchar\bgroup{\RulePremisesNewlineMore[#1]{#2}.{#3}}{\@ifnextchar.{\RulePremisesNewline[#1]{{\begin{array}{c}#2\\#3\end{array}}}}{\RuleMultiPremise[#1]{#2}{#3}}}}

\def \RuleMultiPremise[#1]#2#3{\@ifnextchar\bgroup{\RuleMultiPremise[#1]{#2\premisespacing#3}}{\@ifnextchar.{\RulePremisesNewline[#1]{#2\premisespacing#3}}{\prooftree #2\justifies#3 \using{#1}\endprooftree}}}

\def \RuleWithName[#1]#2{\@ifnextchar\bgroup {\RuleMultiPremise[#1]{#2}}{\@ifnextchar.{\RulePremisesNewline[#1]{#2}}{\prooftree \justifies #2 \using{#1} \endprooftree}}}

\def \RuleWithInfo[#1]{\@ifnextchar[{\RuleWithNameAndCondition[#1]}{\RuleWithName[(#1)]}}

\def \RuleWithNameAndCondition[#1][#2]{\RuleWithName[(#1)^{#2}]}

\def \Inf{\proofrulebaseline=2ex \abovedisplayskip12\point\belowdisplayskip12\point \abovedisplayshortskip8\point\belowdisplayshortskip8\point \@ifnextchar[{\RuleWithInfo}{\RuleWithName[ ]}}

\makeatother

I hope they are useful - if anyone finds any bugs please let me know..

Cheers,

Alex