From 300275364d8fd9b6da6085545073c87d08d94f32 Mon Sep 17 00:00:00 2001 From: Karl Berry Date: Thu, 12 Oct 2006 20:18:11 +0000 Subject: new package bussproofs (12oct06) git-svn-id: svn://tug.org/texlive/trunk@2323 c570f23f-e606-0410-a88d-b1316a301751 --- Master/texmf-dist/doc/latex/bussproofs/testbp2.pdf | Bin 0 -> 51637 bytes Master/texmf-dist/doc/latex/bussproofs/testbp2.tex | 259 +++++++++++++++++++++ 2 files changed, 259 insertions(+) create mode 100644 Master/texmf-dist/doc/latex/bussproofs/testbp2.pdf create mode 100644 Master/texmf-dist/doc/latex/bussproofs/testbp2.tex (limited to 'Master/texmf-dist/doc/latex/bussproofs') diff --git a/Master/texmf-dist/doc/latex/bussproofs/testbp2.pdf b/Master/texmf-dist/doc/latex/bussproofs/testbp2.pdf new file mode 100644 index 00000000000..9aef7cf5f47 Binary files /dev/null and b/Master/texmf-dist/doc/latex/bussproofs/testbp2.pdf differ diff --git a/Master/texmf-dist/doc/latex/bussproofs/testbp2.tex b/Master/texmf-dist/doc/latex/bussproofs/testbp2.tex new file mode 100644 index 00000000000..8bbdef5375a --- /dev/null +++ b/Master/texmf-dist/doc/latex/bussproofs/testbp2.tex @@ -0,0 +1,259 @@ + + + +\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 + +\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} -- cgit v1.2.3