diff options
Diffstat (limited to 'Master/texmf-dist/doc')
| -rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf | bin | 267456 -> 273555 bytes | |||
| -rw-r--r-- | Master/texmf-dist/doc/latex/prftree/prftreedoc.tex | 174 |
2 files changed, 66 insertions, 108 deletions
diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf Binary files differindex ce700a53cce..87e9d490d6a 100644 --- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf +++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.pdf diff --git a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex index 8af679ea760..b28e254b1d5 100644 --- a/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex +++ b/Master/texmf-dist/doc/latex/prftree/prftreedoc.tex @@ -80,9 +80,9 @@ later. The basic command to build a proof tree is \verb|\prftree|. For example, the proof of $A \supset \neg\neg A$ in natural deduction is: \begin{displaymath} - \prftree[r]{$\supset$I} - {\prftree[r]{$\supset$I} - {\prftree[r]{$\supset$E} + \prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{E}$} {\prfboundedassumption{A}} {\prfboundedassumption{\neg A}} {\bot}} @@ -92,14 +92,14 @@ is: This proof is generated by the following \LaTeX{} code: \begin{verbatim} \begin{displaymath} - \prftree[r]{$\supset$I} - {\prftree[r]{$\supset$I} - {\prftree[r]{$\supset$E} - {\prfboundedassumption{A}} - {\prfboundedassumption{\neg A}} - {\bot}} - {\neg\neg A}} - {A \supset \neg\neg A} + \prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{I}$} + {\prftree[r]{$\scriptstyle\supset\mathrm{E}$} + {\prfboundedassumption{A}} + {\prfboundedassumption{\neg A}} + {\bot}} + {\neg\neg A}} + {A \supset \neg\neg A} \end{displaymath} \end{verbatim} @@ -110,8 +110,9 @@ In general, the syntax of the \verb|\prftree| command is: \{\mbox{assumption}_n\}\{\mbox{conclusion}\} \end{displaymath} Assumptions are optional and there may be any number of them. Each -assumption may contain a proof tree, which is typeset -independently. The conclusion is mandatory, and it is supposed to be a +assumption may contain a proof tree, which is typeset independently: +the order allows to use indentation to help reading the source. The +conclusion is mandatory, and it is supposed to be a formula. Assumptions and the conclusion are typeset in a display style math environment. Options control the way the proof is generated: in the example, the \verb|r| option has been used to signal that the @@ -158,39 +159,48 @@ options\footnote{The reader is invited to look at the source code of \begin{array}{lcc@{\qquad}l} \mbox{default (single straight)} & \prftree{A}{B}{A \wedge B} & - \prftree[r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[straight]} \\ \mbox{double straight} & \prftree[d]{A}{B}{A \wedge B} & - \prftree[d,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[double,straight]} \\ \mbox{single dotted} & \prftree[dotted]{A}{B}{A \wedge B} & - \prftree[dotted,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[dotted,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[dotted]} \\ \mbox{double dotted} & \prftree[dotted,d]{A}{B}{A \wedge B} & - \prftree[dotted,d,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[dotted,d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[double,dotted]} \\ \mbox{single dashed} & \prftree[dashed]{A}{B}{A \wedge B} & - \prftree[dashed,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[dashed,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[dashed]} \\ \mbox{double dashed} & \prftree[dashed,d]{A}{B}{A \wedge B} & - \prftree[dashed,d,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[dashed,d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[double,dashed]} \\ \mbox{single fancy} & \prftree[f]{A}{B}{A \wedge B} & - \prftree[f,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[f,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[fancy]} \\ \mbox{double fancy} & \prftree[f,d]{A}{B}{A \wedge B} & - \prftree[f,d,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[f,d,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[double,fancy]} \\ \mbox{noline} & \prftree[noline]{A}{B}{A \wedge B} & - \prftree[noline,r]{$\wedge$I}{A}{B}{A \wedge B} & + \prftree[noline,r]{$\scriptstyle\wedge\mathrm{I}$} + {A}{B}{A \wedge B} & \texttt{[noline]} \end{array} \end{displaymath}\vspace{1ex} @@ -229,8 +239,8 @@ For example, the axiom stating that equality is reflexive, is \end{displaymath} and they are generated by the \LaTeX{} code \begin{displaymath} - \begin{array}{cc} - \verb|\prfaxiom{\forall x\, x = x}|& + \begin{array}{l} + \verb|\prfaxiom{\forall x\, x = x}|\\ \verb|\prfbyaxiom{refl}{\forall x\, x = x}| \end{array} \end{displaymath}\vspace{-.2ex} @@ -249,7 +259,9 @@ For example, \verb|\prfsummary{\forall x\, x = x}| produces \begin{displaymath} \prfsummary{\forall x\, x = x} \end{displaymath} -while \verb|\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}| gives +while +\verb|\prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)}| +gives \begin{displaymath} \prfsummary[name]{A(x)}{B(y)}{B(y) \wedge A(x)} \end{displaymath}\vspace{-.2ex} @@ -700,7 +712,7 @@ may indicate that a label is reused when it should not. The same example can be used to show how the other options work: \begin{displaymath} - \begin{array}{ccc} + \begin{array}{@{}ccc@{}} \begin{prooftree} \prfsummarystyle=2 \prftree[r]{$\vee\mathrm{E}_{\prfref<assum:orEn>}$} @@ -802,7 +814,7 @@ are: {C} \end{prooftree} \end{array} -\end{displaymath}\vspace{.2ex} +\end{displaymath} The \verb|prfassumptioncounter| is the \LaTeX{} counter used to generate the assumption values. It contains the last used value, and @@ -820,7 +832,7 @@ initially, it is set to $0$. By modifying its value, e.g., to \prfboundedassumption<[l]assum:orEff>{B}}{C}} {C} \end{prooftree} -\end{displaymath}\vspace{.2ex} +\end{displaymath} A labelled assumption box is graphically constructed by the package command \verb|\prflabelledassumptionbox| which can be redefined if @@ -933,27 +945,33 @@ calculi: \item \verb|\NDANDER|: conjunction elimination, right; \item \verb|\NDANDEL|: conjunction elimination, left; \item \verb|\NDANDE|: conjunction elimination, unspecified; -\item \verb|\NDIMPI|: implication introduction; -\item \verb|\NDIMPIL|: implication introduction with the label of the - discharged assumption; -\item \verb|\NDIMPE|: implication elimination; \item \verb|\NDORIR|: disjunction introduction, right; \item \verb|\NDORIL|: disjunction introduction, left; \item \verb|\NDORI|: disjunction introduction, unspecified; \item \verb|\NDORE|: disjunction elimination; -\item \verb|\NDOREL|: disjunction elimination with the label of the - discharged assumptions; +\item \verb|\NDOREL|: labelled disjunction elimination; +\item \verb|\NDIMPI|: implication introduction; +\item \verb|\NDIMPIL|: labelled implication introduction; +\item \verb|\NDIMPE|: implication elimination; +\item \verb|\NDNOTI|: negation introduction; +\item \verb|\NDNOTIL|: labelled negation introduction; +\item \verb|\NDNOTE|: negation elimination; \item \verb|\NDALLI|: universal quantifier introduction; \item \verb|\NDALLE|: universal quantifier elimination; \item \verb|\NDEXI|: existential quantifier introduction; \item \verb|\NDEXE|: existential quantifier elimination; -\item \verb|\NDEXE|: existential quantifier elimination with the label - of the discharged assumption; +\item \verb|\NDEXE|: labelled existential quantifier elimination; \item \verb|\NDTI|: truth introduction; \item \verb|\NDFE|: falsity elimination; -\item \verb|\NDLEM|: Law of Excluded Middle. +\item \verb|\NDLEM|: law of Excluded Middle; +\item \verb|\NDAX|: a generic axiom rule. \end{itemize} +The labels, when present, are the first argument, the rest being the +assumptions and, finally, the conclusion. The rules do not have a +fixed format, so extensions are allowed, e.g., on conjunction +elimination or disjunction introduction. + For example, the proof \begin{displaymath} \begin{prooftree} @@ -1228,15 +1246,15 @@ we may consider to define \setcounter{prfsummarycounter}{0} \setcounter{prfassumptioncounter}{0} \mbox{Let } - \vcenter{\vbox{\prfsummary<s:abbrev> + \vcenter{\prfsummary<[f]s:abbrev> {\NDDL{s:notnotA}{\neg\neg A}} {\NDAL{s:notA}{\neg A}} - {\neg\neg A \supset A}}} + {\neg\neg A \supset A}} \equiv - \vcenter{\hbox{$\NDIMPIL{s:notnotA} + \vcenter{\NDIMPIL{s:notnotA} {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}} {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}} - {\neg\neg A \supset A}$}} + {\neg\neg A \supset A}} \end{displaymath} allowing to abbreviate the whole proof as \begin{displaymath} @@ -1254,21 +1272,21 @@ The corresponding \LaTeX{} code is \setcounter{prfsummarycounter}{0} \setcounter{prfassumptioncounter}{0} \mbox{Let } - \vcenter{\vbox{\prfsummary<s:abbrev> + \vcenter{\prfsummary<[f]s:abbrev> {\NDDL{s:notnotA}{\neg\neg A}} {\NDAL{s:notA}{\neg A}} - {\neg\neg A \supset A}}} + {\neg\neg A \supset A}} \equiv - \vcenter{\hbox{$\NDIMPIL{s:notnotA} + \vcenter{\NDIMPIL{s:notnotA} {\NDFE{\NDIMPE{\NDDL{[l]s:notnotA}{\neg\neg A}} {\NDAL{[l]s:notA}{\neg A}}{\bot}}{A}} - {\neg\neg A \supset A}$}} + {\neg\neg A \supset A}} \end{verbatim} for the definition of the proof summary, and \begin{verbatim} \NDOREL{s:notA}{\NDLEM{A \vee \neg A}} {\NDIMPI{\NDDL{[l]s:notA}{A}}{\neg\neg A \supset A}} - {\prfsummary<s:abbrev> + {\prfsummary<[l]s:abbrev> {\NDDL{[l]s:notnotA}{\neg\neg A}} {\NDDL{[l]s:notA}{\neg A}} {\neg\neg A \supset A}} @@ -1627,8 +1645,7 @@ occurrence of a reference, which can be resolved. Most difficulties in the implementation of references lie in the way to construct the boxes to be used in the proof tree. But, the tricky part is the interaction with the \LaTeX{} and \TeX{} kernel for error -reporting. Actually, it is in this part that the bugs signalled in the -next section have their origin. +reporting. % ------------------------------------- \clearpage @@ -1655,66 +1672,7 @@ It is not simple to code such an algorithm in \TeX{}, but the real difficulty is how to represent skylines and how to store them, since \TeX{} provides no abstract data structures. Hence, the implementation of this feature has been postponed to a remote future, or to the will -of a real \TeX{} magician.\vspace{2ex} - -There are three bugs in the packages. - -The first one is that \verb|\mathrm| and similar may break a proof -tree when used in the rule name. I have not been able to track down -why this happens. The effect is that the proof tree is correctly -constructed but it cannot be used as a box, e.g., it cannot be put -inside a \verb|\fbox| or used in normal text. Although disappointing -this bug can be easily circumvented by typesetting the proof tree in a -math environment, e.g., by putting it into a math display or by -enclosing it in a pair of dollar signs.\vspace{2ex} - -The second bug is minimal and in a future version it could be -solved. If one considers the following proof: -\begin{displaymath} - \begin{prooftree} - \fbox{% - \prflineextra=0pt - \prftree - {\prftree - {\prftree - {\prfboundedassumption{\neg\neg A}} - {\prfboundedassumption<bug:1>{\neg A}} - {\bot}} - {A}} - {\neg\neg A \supset A}} - \end{prooftree} -\end{displaymath} -the anchor of assumption (\prfref<bug:1>) is out of the bounding -box. Usually, this is not a problem and, in case, it can be manually -corrected -\begin{displaymath} - \begin{prooftree} - \fbox{% - \prflineextra=0pt - \hbox{\prftree - {\prftree - {\prftree - {\prfboundedassumption{\neg\neg A}} - {\prfboundedassumption<[l]bug:1>{\neg A}} - {\bot}} - {A}} - {\neg\neg A \supset A}\hspace{.34em}}} - \end{prooftree} -\end{displaymath} -as in the following code: -\begin{verbatim} - \prfassumption{\prftree{\prftree{\prftree - {\prfboundedassumption{\neg\neg A}} - {\prfboundedassumption<bug:1>{\neg A}}{\bot}} - {A}}{\neg\neg A \supset A}\hspace{.34em}}} -\end{verbatim}\vspace{2ex} - -The third bug happens the first time a reference is created: if it is -referred by \verb|\prfref| in the rule name, a strange ``immediate'' -follows it. This is not a problem, since the code has to be recompiled -anyway to complete the definition of references, and this is enough to -make the problem to disappear. Since it is a transient problem, I have -not investigated any further. +of a real \TeX{} magician. \vfill |