序贯演算

Question

什么是序贯演算？请参阅 wiki：http://en.wikipedia.org/wiki/Sequent_calculus

所以基本上我想制作这样的东西：

也许使用 Tikz？

Answer 1

看一下

http://www.logicmatters.net/latex-for-logicians/nd/

有一些软件包用于对此类序列进行 teXing。我猜你发布的序列是使用 proof.sty 完成的

Answer 2

由于其他答案只是一个链接，我想我会用该bussproofs包来展示一个示例

\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage{bussproofs}

\newcommand{\implies}{\rightarrow}

\begin{document}
\begin{prooftree}
  \AxiomC{Axiom}
  \UnaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)], Q(a) \vdash Q(a)$}

  \AxiomC{Axiom}
  \UnaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)] \vdash P(a), Q(a)$}
  \RightLabel{$[\neg \vdash]$}
  \UnaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)], \neg P(a) \vdash Q(a)$}

  \RightLabel{$[\lor \vdash]$}
  \BinaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)], \neg P(a) \lor Q(a) \vdash Q(a)$}

  \RightLabel{$[\implies \vdash r.w.]$}
  \UnaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)], P(a) \implies Q(a) \vdash Q(a)$}

  \RightLabel{$[\forall \vdash]$}
  \UnaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)] \vdash Q(a)$}

  \RightLabel{$[\vdash \forall]$}
  \UnaryInfC{$\forall x [P(x)], \forall x [P(x) \implies Q(x)] \vdash \forall x [Q(x)$}
\end{prooftree}
\end{document}

产生如下输出：