path: root/Master/texmf-dist/doc/latex/logic/gn-logic14.tex

%*****************************************************************************/
%*                                                                           */
%*      Version:  1.00   Date: 21/04/92   File: gn-logic14.tex               */
%* Last Version:                          File:                              */
%* Changes:                                                                  */
%* 30/12/90 First version of documentation.                                  */
%* 21/04/92 new properties                                                   */
%*                                                                           */
%* Title:                                                                    */
%* Author: Gerd Neugebauer                                                   */
%*                                                                           */
%* Usage:  latex gn-logic14.tex                                              */
%*                                                                           */
%*****************************************************************************/

\documentstyle[11pt,dina4,gn-logic14]{article}

\setlength{\unitlength}{1pt}


\begin{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newlength{\Width} \Width=\textwidth \advance\Width by -1.5em \divide\Width by 2

\section{The {\tt gn-logic} style option}
Description of Version 1.4 (5/95) by Gerd Neugebauer \bigskip

The {\tt gn-logic} style option provides a facility to typeset logical
formulas of a certain kind. This style option provides an environment like
\verb|eqnarray|, an extended {\tt newtheorem} environment and several macros.



\subsection{Mathematical Symbols}

The following marcos provide better usage of the junctors and quantifiers.
Especially the spacing  is improved.


\noindent\begin{tabular*}{\textwidth}{@{\extracolsep{\fill}}*{4}{l}}
\multicolumn{1}{c}{\small Symbol}
	   & \multicolumn{1}{c}{\small Macro}
			     & 	\multicolumn{2}{c}{\small Example}	  \\
	   &		     &			      & 		  \\
$\AND$	   & \verb|\AND|     & \verb$A\AND B$	      & $A\AND B$	  \\
$\OR$	   & \verb|\OR|	     & \verb$A\OR B$	      & $A\OR B$	  \\
$\XOR$	   & \verb|\XOR|     & \verb$A\XOR B$	      & $A\XOR B$	  \\
$\IMPLIES$ & \verb|\IMPLIES| & \verb$A\IMPLIES B$     & $A\IMPLIES B$	  \\
$\IMPL$	   & \verb|\IMPL|    & \verb$A\IMPL B$	      & $A\IMPL B$	  \\
$\IF$	   & \verb|\IF|	     & \verb$A\IF B$	      & $A\IF B$	  \\
$\IFF$	   & \verb|\IFF|     & \verb$A\IFF B$	      & $A\IFF B$	  \\
$\IFFdef$  & \verb|\IFFdef|  & \verb$A\IFFdef B$      & $A\IFFdef B$	  \\
$\ANDdots$ & \verb|\ANDdots| & \verb$A_1\ANDdots A_n$ & $A_1\ANDdots A_n$ \\
$\ORdots$  & \verb|\ORdots|  & \verb$A_1\ORdots A_n$  & $A_1\ORdots A_n$  \\
$\is$	   & \verb|\is|	     & \verb$x\is y$	      & $x\is y$	  \\
$\Nat$	   & \verb|\Nat|     & \verb$n\in\Nat$	      & $n\in\Nat$	  \\
$\Forall$  & \verb|\Forall|  & \verb$\Forall x P(x)$  & $\Forall x P(x)$  \\
$\Exists$  & \verb|\Exists|  & \verb$\Exists y P(x)$  & $\Exists y P(x)$  \\
\end{tabular*}


\newcommand{\bs}{{\tt\char"5C}}
\newcommand{\mac}[1]{The {\tt\char92 #1} Macro}
\newcommand{\macs}[2]{The {\tt\char92 #1} and the {\tt\char92 #2} Macros}
\newenvironment{compare}%
{\noindent\begin{center}%
  \begin{tabular}{@{}l@{\hspace*{1.5em}produces\hspace*{1.5em}}l@{}}}%
{\end{tabular}\end{center}}

\subsubsection*{\mac{AND}}
This macro can be used for the logical conjunction. In addition to the
\verb|\wedge| macro it adds more space and the formulas tend to be better
readable. Compare

\begin{compare}
\verb$x=1\AND y=x$	& $x=1\AND y=x$		\\
\verb$x=1\wedge y=x$	& $x=1\wedge y=x$	\\
\verb$x=1\land y=x$	& $x=1\land y=x$
\end{compare}

\subsubsection*{\mac{OR}}
This macro can be used for the logical disjunction. In addition to the
\verb|\vee| macro it adds more space. Compare

\begin{compare}
\verb$x=1\OR y=x$	& $x=1\OR y=x$	\\
\verb$x=1\vee y=x$	& $x=1\vee y=x$	\\
\verb$x=1\lor y=x$	& $x=1\lor y=x$
\end{compare}


\subsubsection*{\mac{XOR}}
This macro can be used for the exclusive disjunction. It has no common
counterpart. The spacing is like in in all junctor macros.

\begin{compare}
\verb$x=1\XOR y=x$	& $x=1\XOR y=x$
\end{compare}


\subsubsection*{\macs{IMPL}{IMPLIES}}
These macros can be used for the logical implication. In addition to the
\verb|\rightarrow| macro it adds more space. Compare

\begin{compare}
\verb$x=1\IMPL y=x$		& $x=1\IMPL y=x$	\\
\verb$x=1\IMPLIES y=x$		& $x=1\IMPLIES y=x$	\\
\verb$x=1\rightarrow y=x$	& $x=1\rightarrow y=x$
\end{compare}


\subsubsection*{\mac{IF}}
 This macro can be used for the logical implication written in reverse order.
In addition to the \verb|\leftarrow| macro it adds more space. Compare

\begin{compare}
\verb$x=1\IF y=x$		& $x=1\IF y=x$	\\
\verb$x=1\lefttarrow y=x$	& $x=1\leftarrow y=x$
\end{compare}

\subsubsection*{\mac{IFF}}
 This macro can be used for the logical equivalence.
In addition to the \verb|\leftrightarrow| macro it adds more space. Compare

\begin{compare}
\verb$x=1\IFF y=x$		& $x=1\IFF y=x$	\\
\verb$x=1\leftrighttarrow y=x$	& $x=1\leftrightarrow y=x$
\end{compare}

\subsubsection*{\mac{IFFdef}}
 Like above but with a small ``def'' above the arrow.

\begin{compare}
\verb$x=1\IFFdef y=x$		& $x=1\IFFdef y=x$
\end{compare}

\subsubsection*{\mac{is}}
 This macro is for typesetting unifiers. In this case the predefined
\verb|\setminus| produces to much space.

\begin{compare}
\verb$\{y\setminus x, z\setminus 4\}$	& $\{y\setminus x, z\setminus 4\}$ \\
\verb$\{y\is x, z\is 4\}$		& $\{y\is x, z\is 4\}$		   \\
\verb$\{y\backslash x, z\backslash 4P}$	& $\{y\backslash x, z\backslash 4\}$
\end{compare}

\ifx\AmSTeX\undefined
\def\AmSTeX{$\cal A$\kern-.1667em\lower.5ex\hbox
 {$\cal M$}\kern-.125em$\cal S$-\kern-.1em\TeX}
\fi

\subsubsection*{The Number Macros}
This are macros for those who have no access to the \AmSTeX{} fonts. It makes
the symbols for the natural numbers, integers, rationals, reals and complex
numbers. The usual magnification commands apply to it aswell.


\def\BB#1{\csname bb#1\endcsname}
\def\Line#1{\LINE{#1}\(\BB{#1}_{\BB{#1}}\)}
\def\LINE#1{{\tt \char92bb#1}&%
  {\tiny\BB{#1}}&%
  {\scriptsize\BB{#1}}&%
  {\footnotesize\BB{#1}}&%
  {\small\BB{#1}}&%
  {\normalsize\BB{#1}}&%
  {\large\BB{#1}}&%
  {\Large\BB{#1}}&%
  {\LARGE\BB{#1}}&%
  {\huge\BB{#1}}&%
  {\Huge\BB{#1}}&%
  }
\begin{center}
  \begin{tabular}{c|cccccccccc|c}
    &\multicolumn{10}{|c|}{{\tt \char92tiny \hfill...\hfill\char92normalsize \hfill...\hfill\char92Huge}}&\verb|X_X|
    \\\hline
    \Line B\\
    \verb|\Complex|\Line C\\
    \Line D\\
    \Line E\\
    \Line F\\
    \Line G\\
    \Line H\\
    \Line I\\
    \Line J\\
    \Line K\\
    \Line L\\
    \Line M\\
    \verb|\Nat|  \Line N\\
    \Line O\\
    \Line P\\
    \verb|\Rat|  \Line Q\\
    \verb|\Real| \Line R\\
    \verb|\Int|  \Line Z\\
    \Line{One}
  \end{tabular}
\end{center}

Unfortunately the macros \verb|\bbC|, \verb|\bbG|, \verb|\bbO|, and
\verb|\bbQ| do not scale properly when used in subscripts or superscripts of
formulae. The following examples shows how the sizing can be achieved manually

\noindent\begin{compare}
\verb$\bbQ_{\mbox{\scriptsize \bbQ}}$  & $\bbQ_{\mbox{\scriptsize \bbQ}}$
\end{compare}



\subsubsection*{\macs{Forall}{Exists}}
 The general problem with quantifies is that after the quantified variable the
following formula is not automatically seperated with a small space. This can
be overcome by the following macros.

The \verb|\Forall| and the \verb|\Exists| macros take one argument. They
typeset the respective quantifier followed by the argument (i.e.\ the variable)
and finally a small space. As usual the argument has to be enclosed in braces
if it consists of more than one character. Otherwise the braces can be omitted.
This allows a elegant notation of short quantified formulas.

\noindent\begin{compare}
\verb$\Forall x P(x)$  & $\Forall x P(x)$\\
\verb$\Forall{x_1,\ldots,x_n}P(x_1,\ldots,x_n)$%
&$\Forall{x_1,\ldots,x_n}P(x_1,\ldots,x_n)$\\
\verb$\Exists x P(x)$  & $\Exists x P(x)$\\
\verb$\Exists{x_1,\ldots,x_n}P(x_1,\ldots,x_n)$%
& $\Exists{x_1,\ldots,x_n}P(x_1,\ldots,x_n)$
\end{compare}



\subsection{The {\tt Formula} Environment}

This environment allows to typeset logical formulas. The main problem with the
\verb|eqnarray| environment was the numbering. In multiline formulas my
intention was to have the number in the middle of the formula. Inside this
environment several macros are valid.

\begin{description}
 \item[{\tt\bs begin\{Formula\}[{\em label}] \bs end\{Formula\}}] \ \\
	Start the list of formulas. Optionally a label can be given. This label
	is used to reference the first formula.
 \item[{\tt\bs =}] \ \\
	Start a new line.
 \item[{\tt\bs >}{\em level}] \ \\
	Start a new line and indent to the given {\em level}. This indentation
	is done in quantities of \verb|\FormulaIndent| which can be set with
	the \verb|\setlength| command. The default value is {\tt 3em}.
 \item[{\tt\bs Form[{\em label}]}] \ \\
	Start a new formula. Optionally a {\em label} can be given. This {\em
	label} can be used to reference to the formula (see \verb|\ref|).
\end{description}

Now lets have a look at some examples. First, we see a single two-line formula.
Note that the number at the right side is centered between the two lines.
\medskip

\noindent
\begin{minipage}{\Width}
\small\begin{verbatim}
\begin{Formula}
    P(X) \IMPL
\=  Q(X) \IFF R_1(X) \OR R_2(X)
\end{Formula}
\end{verbatim}
\end{minipage}
\hfill
\begin{minipage}{\Width}
\begin{Formula}
	P(X) \IMPL
\=	Q(X) \IFF R_1(X) \OR R_2(X)
\end{Formula}
\end{minipage}\medskip

Next we will see an example of several formulas. The first formula is split to
three lines and the third line is indented to level 1. Remark: \verb|\=| is in
reality an abbrevation for \verb|\>0|.
\medskip

\noindent
\begin{minipage}{\Width}
\small\begin{verbatim}
\begin{Formula}[form:1]
    P(X) \IMPL
\=  Q(X) \IFF R_1(X)
\>1 \OR R_2(X)
\Form[form:2]
    S(X) \IMPL
\=  \neg Q(X) \IFF R_1(X) \OR R_2(X)
\end{Formula}
\end{verbatim}
\end{minipage}
\hfill
\begin{minipage}{\Width}
\begin{Formula}[form:1]
    P(X) \IMPL
\=  Q(X) \IFF R_1(X)
\>1 \OR R_2(X)
\Form[form:2]
    S(X) \IMPL
\=  \neg Q(X) \IFF R_1(X) \OR R_2(X)
\end{Formula}
\end{minipage}\medskip


\subsection{The {\tt NewTheorem} Environment}

My experience with the {\tt newtheorem} environment was that I had a certain
scheme to use it. First, every theorem got a label. Thus, every {\em theorem}
was followed by a {\tt label} command. Optionally a {\em theorem} may have a
name. This name is typeset right after the number. The body of the {\em
  theorem} allways started in the next line. This let to the definition of an
extended {\tt NewTheorem} environment. The arguments are the same as those of
the {\tt newtheorem} environment. But the environment defined by this extended
command take two optional arguments. The first optional argument is a label to
be assigned to the {\em theorem}. This argument has to be enclosed in
parentheses. The second type of optional argument has to be enclosed in
brakets. It is typeset in \verb|\small| after the title text. The third
optional argument is enclosed in \verb|<>|. It is typeset in \verb|\small\bf|
and surrounded by parentheses.
\medskip

\noindent\begin{minipage}{\Width}
\small\begin{verbatim}

\NewTheorem{guess}{Conjecture}

\begin{guess}[Fermat](thm:fermat)
 There do not exist integers $n>2$,
 $x$, $y$, and $z$ such that
 $x^n+y^n=z^n$.
\end{guess}
\end{verbatim}
\end{minipage}
\hfill
\begin{minipage}{\Width}
\NewTheorem{guess}{Conjecture}

\begin{guess}[Fermat](thm:fermat)
 There do not exist integers $n>2$,
 $x$, $y$, and $z$ such that
 $x^n+y^n=z^n$.
\end{guess}
\end{minipage}
\medskip

The commands used to typeset some of the optional argument can be customized
in the following way. The macros \verb|\TheoremTitle| and \verb|\TheoremName|
are used to typeset their argument in \verb|\small| and \verb|\small\bf| and
enclosed in parentheses respectively. This macros can be redefined using
\verb|\renewcommand| as shown in the following example:
\medskip

\noindent\begin{minipage}{\Width}
\footnotesize\begin{verbatim}
\NewTheorem{theorem}{Theorem}
\renewcommand{\TheoremTitle}[1]{{\sf [#1]}}
\renewcommand{\TheoremName}[1]{{\small(#1)}}
\begin{theorem}[Fermat]<conjecture>(thm:f2)
 There do not exist integers ...
\end{theorem}
\end{verbatim}
\end{minipage}
\hfill
\begin{minipage}{\Width}
\NewTheorem{theorem}{Theorem}
\renewcommand{\TheoremTitle}[1]{{\sf #1}}
\renewcommand{\TheoremName}[1]{{\small(#1)}}
\begin{theorem}[Fermat]<conjecture>(thm:f2)
 There do not exist integers $n>2$,
 $x$, $y$, and $z$ such that
 $x^n+y^n=z^n$.
\end{theorem}
\end{minipage}

\end{document}



\newcommand{\ENTRY}[1]{{#1 \Nat}& {#1 \Int}& {#1 \Rat}&{#1 \Real}& {#1 \Complex}}

\begin{center}
\begin{tabular}{l|ccccc}
&\verb|\Nat|&\verb|\Int|&\verb|\Rat|&\verb|\Real|&\verb|\Complex|\\
&&\\\hline&&\\
\verb$\tiny$		& \ENTRY{\tiny}		\\
\verb$\scriptsize$	& \ENTRY{\scriptsize}	\\
\verb$\footnotesize$	& \ENTRY{\footnotesize} \\
\verb$\small$		& \ENTRY{\small}	\\
\verb$\normalsize$	& \ENTRY{\normalsize}	\\
\verb$\large$		& \ENTRY{\large}	\\
\verb$\Large$		& \ENTRY{\Large}	\\
\verb$\LARGE$		& \ENTRY{\LARGE}	\\
\verb$\huge$		& \ENTRY{\huge}		\\
\verb$\Huge$		& \ENTRY{\Huge}
\end{tabular}\end{center}