Add bussproofs for inference rules and other logical proofs

[Ailrun]

Link: https://www.ctan.org/pkg/bussproofs

Even though it is possible to write simple inference rules and logical proofs with array env and \frac, \cfrac, etc., it becomes significantly hard to write complex rules and proofs with those commands.

[DXsmiley]

I'm not familiar with this package. Can you show me some sample code and output so I can see what it does?

[Ailrun]

Sure. I will post it as soon as I can access my PC.

[Ailrun]

With this code

\begin{prooftree}
  \AxiomC{A}
  \AxiomC{B}
  \AxiomC{C}
  \BinaryInfC{D}
  \BinaryInfC{E}
\end{prooftree}

the package gives

[Ailrun]

If you don't like the package, I think https://www.ctan.org/pkg/ebproof would also work for the task.

In that package, the following code

\begin{prooftree}
  \infer0{\vdash A}
  \hypo{\vdash B} \infer1{\vdash B, C}
  \infer2{\vdash A \wedge B, C}
\end{prooftree}

is rendered as

[Ailrun]

@DXsmiley any updates?