标记校样的各个部分

Question

我在用着总线防护布局序列演算证明。我想标记一些推论的部分内容。例如，给出以下证明：

\begin{prooftree}
\AxiomC{$X\vdash\phi\rightarrow\psi$}
\AxiomC{$Y\vdash\phi$}
\BinaryInfC{$X;Y\vdash\psi$}
\end{prooftree}

我想将假设标记为假设，将结论标记为结论。理想情况下，我想使用上括号和下括号来实现这一点。例如，我想用一个横跨假设的上括号，并在上括号上方加上“假设”一词。

现在，出于贪心，我还想要其他的东西：我想要放置标记推理部分的箭头，例如，指向的箭头，其$\vdash$底部有单词“旋转栅门”，或者指向“；”的箭头，其底部有单词“标点符号”。

部分解决方案受到热烈欢迎，我在这里要求很多。

Answer 1

以下是使用 TikZ 库的方法tikzmark：

\documentclass{article}
\usepackage{tikz}
\usetikzlibrary{tikzmark,decorations.pathreplacing,calc}
\usepackage{bussproofs}
\begin{document}
\begin{prooftree}
  \AxiomC{\tikzmark{a}$X\vdash\phi\rightarrow\psi$\tikzmark{b}}
  \AxiomC{\tikzmark{c}$Y\vdash\phi$\tikzmark{d}}
  \BinaryInfC{\tikzmark{e}$X\tikzmark{e1};\tikzmark{f1}Y\tikzmark{e2}\vdash\tikzmark{f2}\psi$\tikzmark{f}}
\end{prooftree}
\begin{tikzpicture}[remember picture, overlay]
  \draw [decorate, decoration={brace, amplitude=7.5pt}] ({pic cs:a}) +(0,\baselineskip) coordinate (g) -- (g -| {pic cs:d}) node [midway, above, anchor=south, yshift=5pt] {Hypotheses};
  \draw [decorate, decoration={brace, amplitude=7.5pt}] ({pic cs:f}) +(0,-.5\baselineskip) coordinate (h) -- (h -| {pic cs:e}) node [midway, below, anchor=north, yshift=-7.5pt] {Conclusion};
  \draw [<-] ($({pic cs:e2})!1/2!({pic cs:f2})$) coordinate (i) -- ([yshift=-1.25\baselineskip]{{pic cs:d} |- i}) node (j) [right] {Turnstile};
  \draw [<-] ({pic cs:e1})  +(0,-1.5pt) -- (j -| {pic cs:a}) node [left] {Punctuation};
\end{tikzpicture}
\end{document}

Answer 2

我不是个做证明的人，也没有图片，所以我只能猜测如何解释 OP 的请求。以下是我的猜测。

我引入了\pointupat[<alignment>]{math content}{text description}以及\ltxtoverbrace{<length>}{text description}。显然，\pointdownat也可以类似地编写宏。

这是 MWE。

\documentclass{article}
\usepackage{bussproofs,amsmath,stackengine}
\newcommand\pointupat[3][c]{\def\useanchorwidth{T}\def\stackalignment{c}%
  \def\stacktype{L}\setstackgap{L}{.8\baselineskip}%
  \ensurestackMath{\stackunder{{}#2{}}{\def\stackalignment{#1}%
  \stackunder{\uparrow}{\scriptstyle\text{#3}}}}}
\newcommand\ltxtoverbrace[2]{%
  \rlap{$\overbrace{\strut\rule{#1}{0pt}}^{\text{#2}}$}
}
\begin{document}
\begin{prooftree}
\AxiomC{$\ltxtoverbrace{23ex}{hypotheses}X\vdash\phi\rightarrow\psi$}
\AxiomC{$Y\vdash\phi$}
\BinaryInfC{$\underbrace{X;Y\vdash\psi}_{\text{conclusion}}$}
\end{prooftree}
\begin{prooftree}
\AxiomC{$\overbrace{X\vdash\phi\rightarrow\psi}^{\text{hypothesis}}$}
\AxiomC{$Y\vdash\phi$}
\BinaryInfC{$X\pointupat[r]{;}{punctuation}Y\pointupat[l]{\vdash}{turnstile}\psi$}
\end{prooftree}
\end{document}