3

The proof package's \infer command automatically sizes the lines it draws.

However, it isn't always right (pdflatex output):

enter image description here

The line is too short on the left.

Is this a package bug/inaccuracy, or am I doing something wrong?

Here is the code (MWE made) that produced the document above:

\documentclass{article}
%
\usepackage{proof}
%
\begin{document}
\[
 \infer{\bot}{
   \infer{P}{
     \infer{P \vee P}{
       P \vee Q
       \quad
       P \vee \neg Q
     }
   }
  \qquad
  \infer{\neg P}{
   \infer{\neg P \vee \neg P}{
     \neg P \vee Q
     \quad
     \neg P \vee \neg Q
   }
  }
 }
\]
\end{document}
2
  • 2
    After looking for some implementation code for \infer, and not finding anything; I suggest that the third line is space-sensitive. Since the right column is larger (added negative symbols) than the left, it is "read" as incomplete, thus is made shorter at the base connection. By intuition, my advice is to substitute in the left column code \quad with \qquad, this will add horizontal space and the line will cover the letter base. – TheVal Nov 18 '13 at 13:30
  • You might have a look at bussproofs.sty of which you find a guide at logicmatters.net/latex-for-logicians/nd – egreg Nov 18 '13 at 14:58
3

You may have a look at bussproofs.sty; you find also an online guide

Here's a comparison (I added \qquad as suggested by Andrea L. for making the first line slightly wider)

\documentclass{article}
\usepackage{proof}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
\AxiomC{$P\lor Q$} \AxiomC{$P\lor\lnot Q$}
\BinaryInfC{$P\lor P$}
\UnaryInfC{$P$}
\AxiomC{$\lnot P\lor Q$} \AxiomC{$\lnot P\lor \lnot Q$}
\BinaryInfC{$\lnot P\lor\lnot P$}
\UnaryInfC{$\lnot P$}
\BinaryInfC{$\bot$}
\end{prooftree}
\[
 \infer{\bot}{
   \infer{P}{
     \infer{P \vee P}{
       P \vee Q
       \qquad
       P \vee \neg Q
     }
   }
  \qquad
  \infer{\neg P}{
   \infer{\neg P \vee \neg P}{
     \neg P \vee Q
     \quad
     \neg P \vee \neg Q
   }
  }
 }
\]
\end{document}

enter image description here

3
  • Glad to have left a useful suggestion posted inside an answer! – TheVal Nov 18 '13 at 16:35
  • @AndreaL. You may add your answer based on proof – egreg Nov 18 '13 at 16:37
  • The only thing that is stopping me to do that is the lack of documentation, since I do not know any buliding feature of \infer I don't want to leave tips that my cause errors with other situations. – TheVal Nov 18 '13 at 16:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.