0

I have tried a few packages to align inference rules but I have not figured out how to avoid the following problem. My proof tree looks like this:

 A ------------------------- B ----- D C

but should look like this:

 A ------------------------- B C ----- D

Do you have any advice for a package that supports that alignment? Specifically can I use \infer for this somehow? I tried to include a minimum working example but when I minimize the proof tree is not even working for the above anymore and I don't seem to be able to figure out why. I also tried bussproofs unsuccessfully.

Improve this question
3
  • 1
    Welcome! In the future, please always include a small example i.e. code. For example, you could have included your attempt to use bussproofs. That gives people a starting point, even if it doesn't work. Also, please say what doesn't work. Do you get an error? Which? Does it compile but give the wrong output? What's wrong? Etc. Commented Oct 8, 2023 at 21:40
  • Where is \infer from? I'm not sure if you mean the \infer1 etc. from ebproof or something else? Commented Oct 8, 2023 at 21:41
  • 1
    Thanks you both. Sorry, about the missing example. I made a bunch of changes and suddenly even the tree above (that I managed to generate with different packages) would not work anymore and I did not know how to get it back. Commented Oct 8, 2023 at 22:05

2 Answers 2

Reset to default
1

For the kind of proof you're drawing, you need to tell bussproofs to turn the tree upside down. This can be done with the \rootAtTop command. If all of your proofs look like this, then you can set the root globally using the command \alwaysRootAtTop in the preamble, in which case you don't need to specify it for each proof.

\documentclass{article} \usepackage{bussproofs} \begin{document} \begin{prooftree} \rootAtTop \AxiomC{D} \UnaryInfC{B} \AxiomC{C} \BinaryInfC{A} \end{prooftree} \end{document}

output of code

Improve this answer
1

A more recent alternative to bussproofs is ebproof. This was basically written to overcome certain limitations in bussproofs and because its author didn't like all of the decisions implemented in bussproofs's design.

Example using ebproof for an inline and a displayed proof:

ebproof inline and display

\documentclass{article} \usepackage{ebproof} \begin{document} \begin{prooftree} [proof style=downwards] \hypo{D} \infer1{B} \hypo{C} \infer2{A} \end{prooftree} \begin{prooftree}* [proof style=downwards] \hypo{D} \infer1{B} \hypo{C} \infer2{A} \end{prooftree} \end{document}

However, I recommend defining semantic markup for the symbols you need and avoiding the direct use of names such as \vdash found in ebproof's manual. Alternatively, use the turnstile package.

Improve this answer

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.