summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/bussproofs/testbp2.tex
diff options
context:
space:
mode:
authorNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
committerNorbert Preining <norbert@preining.info>2019-09-02 13:46:59 +0900
commite0c6872cf40896c7be36b11dcc744620f10adf1d (patch)
tree60335e10d2f4354b0674ec22d7b53f0f8abee672 /macros/latex/contrib/bussproofs/testbp2.tex
Initial commit
Diffstat (limited to 'macros/latex/contrib/bussproofs/testbp2.tex')
-rw-r--r--macros/latex/contrib/bussproofs/testbp2.tex321
1 files changed, 321 insertions, 0 deletions
diff --git a/macros/latex/contrib/bussproofs/testbp2.tex b/macros/latex/contrib/bussproofs/testbp2.tex
new file mode 100644
index 0000000000..3dd30d98bd
--- /dev/null
+++ b/macros/latex/contrib/bussproofs/testbp2.tex
@@ -0,0 +1,321 @@
+
+
+
+\documentclass[12pt]{article}
+\usepackage{bussproofs}
+\usepackage{amssymb}
+\usepackage{latexsym}
+
+% This is the "centered" symbol
+\def\fCenter{{\mbox{\Large$\rightarrow$}}}
+
+% Optional to turn on the short abbreviations
+\EnableBpAbbreviations
+
+% \alwaysRootAtTop % makes proofs upside down
+% \alwaysRootAtBottom % -- this is the default setting
+
+\begin{document}
+\thispagestyle{empty}
+
+When the {\tt bussproofs.sty} code was first written, the
+only documention for the {\tt bussproofs} style was in the
+comments at the beginning of the style file {\tt bussproofs.sty}.
+But recently (July 2004), Peter Smith has written an excellent
+exposition of {\tt bussproofs.sty}, presently available
+at
+\begin{center}
+\tt
+http://www.phil.cam.ac.uk/teaching\_staff/Smith/LaTeX/nd.html
+\end{center}
+
+The present document is
+a sample \LaTeX{} file that was created for testing
+purposes while writing the {\tt bussproofs} code and you might
+find that it useful as an example of how to
+use special features of the style.
+
+Author: Sam Buss \hspace*{1in} Email: {\tt sbuss@ucsd.edu}.
+\vspace*{0.25in}
+
+Here is some text.
+\begin{center}
+\Axiom$\Gamma^\prime\fCenter\Delta,A,A$
+\LeftLabel{Weakening}\RightLabel{}
+\UnaryInf$\lnot A,\Gamma^\prime \fCenter \Delta, A$
+\LeftLabel{.}\RightLabel{\small $\lor$:right}
+\UnaryInf$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\LeftLabel{eigenvariable $x$}\RightLabel{$\forall$:right}
+\UnaryInf$\Gamma \fCenter \Delta$
+\DisplayProof
+\end{center}
+Here is more text.
+\begin{prooftree}
+\alwaysDashedLine
+\alwaysDoubleLine
+\Axiom$\Delta\fCenter\Pi$
+\Axiom$\Gamma^\prime\fCenter\Delta,A$
+\dottedLine
+\singleLine
+\UnaryInf$\lnot A,\Gamma^\prime \fCenter \Delta$
+\UnaryInf$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\singleLine
+\UnaryInf$\Gamma \fCenter \Delta$
+\BinaryInf$\Gamma,\Pi,A \fCenter \Delta, \Delta,B$
+\Axiom$\fCenter\mbox{\rm Hi there}$
+\singleLine
+\BinaryInf$\Gamma\fCenter\Delta$
+\end{prooftree}
+\begin{center}
+\alwaysDoubleLine
+\AX$\Delta\fCenter\Pi$
+\AX$\Gamma^\prime\fCenter\Delta,A$
+\singleLine
+\UI$\lnot A,\Gamma^\prime \fCenter \Delta$
+\UI$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\singleLine
+\UI$\Gamma \fCenter \Delta$
+\LL{.}\RightLabel{$\lor$:left}
+\BI$\Gamma,\Pi,A \fCenter \Delta, \Delta,B$
+\AXC{Hi there}
+\singleLine
+\BI$\Gamma\fCenter\Delta$
+\DisplayProof
+\end{center}
+The above examples show `displayed' proofs.
+On the other hand,
+for putting proofs inline instead of displayed,
+it is also permissable to put proofs into text rather than into
+centered environments. For example, one can write a proof right
+here:
+\centerAlignProof %Which ever one of these is LAST sets the vertical alignment
+\bottomAlignProof %Try commenting out all but one of these three lines.
+\normalAlignProof
+\Axiom$\Gamma^\prime\fCenter\Delta,A$
+\doubleLine
+\UnaryInf$\lnot A,\Gamma^\prime \fCenter \Delta$
+\UnaryInf$\lnot A,\lnot A,\Gamma^\prime \fCenter \Delta$
+\doubleLine
+\UnaryInf$\Gamma \fCenter \Delta$
+\Axiom$\Delta\fCenter\Pi$
+\kernHyps{-.5in}\insertBetweenHyps{\hskip-.25in}
+\BinaryInf$\Gamma,\Pi,A \fCenter \Delta, \Delta,B$
+\Axiom$\fCenter\mbox{\rm Hi there}$
+\doubleLine
+\BinaryInf$\Gamma\fCenter\Delta$
+\DisplayProof{} %% NOTE THE USE OF "{}"
+although of course the proof is quite big compared to the text.
+There is no reason you could not add \verb+\subscriptstyle+ or \verb+\small+
+commands to the lines of the proofs to shrink things down.
+The previous proof looks strange because it is illustrated the usage
+of \verb+\kernHyps+ and \verb+\insertBetweenHyps+. Finally
+a 3-ary inference with a usage of \verb+\noLine+ is:
+\begin{prooftree}
+\AxiomC{$A\lor B$}
+\AxiomC{$[A]$}
+\noLine
+\UnaryInfC{$C$}
+\AxiomC{$[B]$}
+\noLine
+\UnaryInfC{$C$}
+\TrinaryInfC{$C$}
+\end{prooftree}
+
+
+Two more examples:
+\begin{center}
+\AxiomC{A,B} \AxiomC{C} \BIC{A-B-C}
+\AXC{good} \AXC{bad} \BIC{$\frac{good}{bad}$A}
+\BIC{done}
+\DP
+\end{center}
+
+\begin{center}
+\Axiom$\fCenter A,B$ \Axiom$\fCenter C$ \BI$\fCenter A-B-C$
+\AX$\fCenter good$ \AX$\fCenter bad$ \BI$\fCenter\frac{good}{bad}A$
+\BI$\fCenter done$
+\DP
+\end{center}
+
+
+Small labels can be created as in the third proof below:
+\[
+\AxiomC{A}
+\RightLabel{1}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\quad
+\AxiomC{A}
+\RightLabel{(2)}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\quad
+\AxiomC{A}
+\RightLabel{\scriptsize(3)}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\quad
+\AxiomC{A}
+\LeftLabel{(4)}
+\UnaryInfC{$\bot$}
+\DisplayProof
+\]
+Arnold's example of inline proof: The figure
+\AxiomC{$\dots\Gamma_\iota\dots(\iota\in I)$}
+\RightLabel{$I$}
+\UnaryInfC{$\Gamma$}
+\DisplayProof{}
+is called ...
+%% NOTE THE USE OF "{}" after \DisplayProof to keep LaTeX from eating subsequent spaces!
+
+\bigskip
+
+\noindent{\bf Upside down proofs}
+Proofs can be rendered upside down. For instance the proof above with
+a 3-ary inference can be made upside down by giving the command
+\verb+\rootAtTop+. This is useful if you want your proof trees to have
+their root at the top.
+
+\alwaysRootAtTop % Henceforth puts the root at the top
+
+\begin{prooftree}
+\AxiomC{$A\lor B$}
+\AxiomC{$[A]$}
+\noLine
+\UnaryInfC{$C$}
+\AxiomC{$[B]$}
+\noLine
+\UnaryInfC{$C$}
+\TrinaryInfC{$C$}
+\end{prooftree}
+
+To make the change permanent for the rest of your document, use the
+command \verb+\alwaysRootAtTop+
+
+\bigskip
+
+\noindent
+Another upside-down example, from Alex Hertel:
+\bigskip
+
+\hbox{\kern-2cm%
+\tiny
+\rootAtTop
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (1 \wedge 1) \vee 0 ) \vee ( (0 \wedge 0) \vee 0 ) )$}
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (1 \wedge 1) \vee 1 ) \vee ( (0 \wedge 0) \vee 1 ) )$}
+\LeftLabel{$[0/z]$}
+\RightLabel{$[1/z]$}
+\BinaryInfC{$\forall z ( ( (1 \wedge 1) \vee z ) \vee ( (0 \wedge 0) \vee z ) )$}
+\RightLabel{$[0/y]$}
+\UnaryInfC{$\exists y \forall z ( ( (1 \wedge \neg y) \vee z ) \vee ( (0 \wedge y) \vee z ) )$}
+\RightLabel{$[0/y]$}
+\UnaryInfC{$\exists y \forall z ( ( (1 \wedge \neg y) \vee z ) \vee ( (0 \wedge y) \vee z ) )$}
+
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (0 \wedge 0) \vee 0 ) \vee ( (1 \wedge 1) \vee 0 ) )$}
+\AxiomC{$= 1$}
+\noLine
+\UnaryInfC{$( ( (0 \wedge 0) \vee 1 ) \vee ( (1 \wedge 1) \vee 1 ) )$}
+\LeftLabel{$[0/z]$}
+\RightLabel{$[1/z]$}
+\BinaryInfC{$\forall z ( ( (0 \wedge 0) \vee z ) \vee ( (1 \wedge 1) \vee z ) )$}
+\RightLabel{$[1/y]$}
+\UnaryInfC{$\exists y \forall z ( ( (0 \wedge \neg y) \vee z ) \vee ( (1 \wedge y) \vee z ) )$}
+
+\LeftLabel{$[0/x]$}
+\RightLabel{$[1/x]$}
+\BinaryInfC{$\forall x \exists y \forall z ( ( (\neg x \wedge \neg y) \vee z ) \vee ( (x \wedge y) \vee z ) )$}
+\DisplayProof
+} % End of \hbox
+
+\bigskip
+
+
+\alwaysRootAtBottom
+Testing of quaternary and quinary inferences (a bit scrunched due a use of
+\verb+\insertBetweenHyps+):
+\begin{prooftree}
+\insertBetweenHyps{\hskip-1em}
+\AxiomC{$A^B$}
+\Axiom$A_B\fCenter A_{B_C}$
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuinaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\insertBetweenHyps{\hskip-1em}
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuaternaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\end{prooftree}
+
+\alwaysRootAtTop
+Testing of quaternary and quinary inferences (a bit scrunched due a use of
+\verb+\insertBetweenHyps+):
+\begin{prooftree}
+\insertBetweenHyps{\hskip-1em}
+\AxiomC{$A^B$}
+\Axiom$A_B\fCenter A_{B_C}$
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuinaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\insertBetweenHyps{\hskip-1em}
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\QuaternaryInf$X\fCenter XXXXX$
+\UnaryInf$YYYY\fCenter Y$
+\end{prooftree}
+
+\begin{prooftree}
+\insertBetweenHyps{\hskip-1em}
+\Axiom$A^B\fCenter A^{B^C}$
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\TrinaryInf$X\fCenter XXXXX$
+\end{prooftree}
+
+\newenvironment{proof}{\begin{trivlist}\item[]{\bf Proof\ }}%
+{\end{trivlist}}
+\newenvironment{proofX}{\noindent{\bf Proof\ }}%
+{}
+
+\begin{proofX}
+\begin{prooftree}
+\Axiom$A^{B^C}\fCenter A^{B^{C^D}}$
+\Axiom$A^{B^{C^D}}\fCenter A^{B^{C^{D^E}}}A^{B^{C^{D^E}}}$
+\BinaryInf$X\fCenter XXXXX$
+\end{prooftree}
+\end{proofX}
+
+\newbox\gnBoxA
+\newdimen\gnCornerHgt
+\setbox\gnBoxA=\hbox{$\ulcorner$}
+\global\gnCornerHgt=\ht\gnBoxA
+\newdimen\gnArgHgt
+
+\def\Godelnum #1{%
+ \setbox\gnBoxA=\hbox{$#1$}%
+ \gnArgHgt=\ht\gnBoxA%
+ \ifnum \gnArgHgt<\gnCornerHgt
+ \gnArgHgt=0pt%
+ \else
+ \advance \gnArgHgt by -\gnCornerHgt%
+ \fi
+ \raise\gnArgHgt\hbox{$\ulcorner$} \box\gnBoxA %
+ \raise\gnArgHgt\hbox{$\urcorner$}}
+
+This last sentence has nothing to do with proof trees, but shows my
+macros for G\"odel number delimeters:
+$\Godelnum A, \Godelnum B$
+$\Godelnum s$
+\end{document}