% -*- TeX:DE -*-
%%% ====================================================================
%%% @LaTeX-file $RCSfile: SyntaxParser.java,v $
%%% $Revision: 1.16 $
%%% ====================================================================

%%% This document was generated by class org.qedeq.parse.SyntaxParser
%%% at 2004-09-26T17:49:24+0200.

%%% Project Principia Mathematica II - *pmii* - http://www.qedeq.org
%%% Copyright 2001, 2002 Michael Meyling (michael@meyling.com)

%%% This file is part of *pmii*.

%%% Permission is granted to copy, distribute and/or modify this document
%%% under the terms of the GNU Free Documentation License, Version 1.2
%%% or any later version published by the Free Software Foundation;
%%% with no Invariant Sections, no Front-Cover Texts, and no
%%% Back-Cover Texts.

\documentclass[a4paper,german,10pt,twoside]{article}

\usepackage[german]{babel}
\usepackage{makeidx}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{color}
\usepackage{epsfig,longtable}

\addtolength{\textheight}{\baselineskip} \addtolength{\topmargin}{-5\baselineskip}

\setlength{\parindent}{0pt}
\frenchspacing \sloppy

%       Math definitions
\newcommand{\deft}{:=}
\newcommand{\defp}{\ :\Leftrightarrow \ }
\newcommand{\impl}{\ \Rightarrow \ }
\newcommand{\equi}{\ \Leftrightarrow \ }
\newcommand{\conj}{\ \wedge \ }
\newcommand{\disj}{\ \vee \ }
\newcommand{\err}{
 \begin{minipage}{\linewidth}
 $\hspace*{2.5pt} \angle \vspace*{-5.5pt} \\ \swarrow$
 \end{minipage}
}
\newcommand{\stimes}{\stackrel{\rm S} \times}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\newcommand{\class}[2]{\left\lfloor #1 \right\rfloor_{#2}}

\DeclareMathOperator{\id}{id} \DeclareMathOperator{\Power}{\mathfrak P}
\DeclareMathOperator{\isSet}{\mathfrak M}


\begin{document}

This text defines the format of a qedeq module file for the rule version
1.00.00. Such a file contains ASCII characters and has a lisp like
structure. There are two kinds of axioms: integers and strings.
Strings are quoted (") that means strings are surrounded by quotes (")
and quotes inside the strings are escaped by doubling them.
All other types are lists preceded by an function operator. These
lists are surrounded by brackets and contain a sequence of elements,
separated by commas. Each element is an atom or further operator
lists. E.g.:
\vspace*{0.2cm}
\par
{\qquad \tt AND(PROP(1), OR(PROP(2), PROP(3)))}
\par
\vspace*{0.2cm}
The following text shows the structure of a qedeq module file in BNF 
notation.
\par
\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$MODULE$\rangle$} & & start terminal for qedeq module format\\
{\tt ~~$::=$~'MODULE('} & \\
 & {\tt ~$\langle$HEADER$\rangle$,} & header\\
 & {\tt ~[$\langle$IMPORTS$\rangle$],} & needed other qedeq modules\\
 & {\tt ~[$\langle$USEDBY$\rangle$],} & this qedeq module is used by\\
 & {\tt ~$\langle$PARAGRAPHS$\rangle$} & paragraphs with axioms, propositions etc.\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$HEADER$\rangle$} & & header of a qedeq module\\
{\tt ~~$::=$~'HEADER('} & \\
 & {\tt ~$\langle$SPEC$\rangle$,} & specification of this module\\
 & {\tt ~$\langle$HEADLINE$\rangle$,} & title of this module\\
 & {\tt ~$\langle$DESCRIPTION$\rangle$,} & abstract\\
 & {\tt ~$\langle$EMAIL$\rangle$,} & email address of module administrator\\
 & {\tt ~$\langle$AUTHORS$\rangle$} & authors of this module\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$SPEC$\rangle$} & & specification of a qedeq module\\
{\tt ~~$::=$~'SPEC('} & \\
 & {\tt ~$\langle$NAME$\rangle$,} & name of qedeq module\\
 & {\tt ~$\langle$VERSION$\rangle$,} & version of qedeq module\\
 & {\tt ~$\langle$VERSION$\rangle$,} & needed rule version\\
 & {\tt ~$\langle$LOCATIONS$\rangle$} & list of absolute or relative URLs, the specified module could be found, only the path to the module should stand here, the file name is: $\langle$NAME$\rangle\_\langle$VERSION$\rangle\_\langle$VERSION$\rangle$.qedeq\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$NAME$\rangle$} & & name\\
{\tt ~~$::=$~'NAME('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$text$\rangle$} & & text atom, an arbitrary string\\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$VERSION$\rangle$} & & version nummer in format nn.nn.nn\\
{\tt ~~$::=$~'VERSION('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$LOCATIONS$\rangle$} & & list of qedeq module URLs\\
{\tt ~~$::=$~'LOCATIONS('} & \\
 & {\tt ~$\langle$LOCATION$\rangle$,} & at least one URL must be there\\
 & {\tt ~\{$\langle$LOCATION$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$LOCATION$\rangle$} & & relative or absolute URL, which points to the directory of an qedeq module file\\
{\tt ~~$::=$~'LOCATION('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$HEADLINE$\rangle$} & & title of a qedeq module\\
{\tt ~~$::=$~'HEADLINE('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$DESCRIPTION$\rangle$} & & description of qedeq module (''abstract'')\\
{\tt ~~$::=$~'DESCRIPTION('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$EMAIL$\rangle$} & & email address\\
{\tt ~~$::=$~'EMAIL('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$AUTHORS$\rangle$} & & author list\\
{\tt ~~$::=$~'AUTHORS('} & \\
 & {\tt ~$\langle$AUTHOR$\rangle$,} & \\
 & {\tt ~\{$\langle$AUTHOR$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$AUTHOR$\rangle$} & & \\
{\tt ~~$::=$~'AUTHOR('} & \\
 & {\tt ~$\langle$text$\rangle$,} & author name\\
 & {\tt ~$\langle$EMAIL$\rangle$} & email address of author\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$IMPORTS$\rangle$} & & list of imported modules\\
{\tt ~~$::=$~'IMPORTS('} & \\
 & {\tt ~$\langle$IMPORT$\rangle$,} & \\
 & {\tt ~\{$\langle$IMPORT$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$IMPORT$\rangle$} & & informations about an import module\\
{\tt ~~$::=$~'IMPORT('} & \\
 & {\tt ~$\langle$SPEC$\rangle$,} & module specification\\
 & {\tt ~$\langle$LABEL$\rangle$} & alias name for an imported module\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$LABEL$\rangle$} & & label for referencing\\
{\tt ~~$::=$~'LABEL('} & \\
 & {\tt ~$\langle$text$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$USEDBY$\rangle$} & & list of modules, which use this one\\
{\tt ~~$::=$~'USEDBY('} & \\
 & {\tt ~$\langle$SPEC$\rangle$,} & \\
 & {\tt ~\{$\langle$SPEC$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PARAGRAPHS$\rangle$} & & paragraphs\\
{\tt ~~$::=$~'PARAGRAPHS('} & \\
 & {\tt ~$\langle$PARAGRAPH$\rangle$,} & \\
 & {\tt ~\{$\langle$PARAGRAPH$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PARAGRAPH$\rangle$} & & paragraph\\
{\tt ~~$::=$~'PARAGRAPH('} & \\
 & {\tt ~$\langle$LABEL$\rangle$,} & reference anchor\\
 & {\tt ~[$\langle$text$\rangle$],} & LaTeX text\\
 & {\tt ~( } & \\
 & {\tt ~~$\langle$ABBREVIATION$\rangle$ |} & \\
 & {\tt ~~$\langle$AXIOM$\rangle$ |} & \\
 & {\tt ~~$\langle$DECLARERULE$\rangle$ |} & \\
 & {\tt ~~$\langle$PROPOSITION$\rangle$} & \\
  &  {\tt ~),} & or list\\
 & {\tt ~[$\langle$text$\rangle$]} & LaTeX text\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$ABBREVIATION$\rangle$} & & definition of an abbreviation\\
{\tt ~~$::=$~'ABBREVIATION('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$,} & operator to be defined with pattern variables\\
 & {\tt ~$\langle$FORMULA$\rangle$} & definition for the operator, the same pattern variables as before must occur\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$FORMULA$\rangle$} & & formula of predicate calculus\\
 & {\tt ~( } & \\
 & {\tt ~~$\langle$PROP$\rangle$ |} & proposition variable\\
 & {\tt ~~$\langle$NOT$\rangle$ |} & negation\\
 & {\tt ~~$\langle$AND$\rangle$ |} & conjunction (logical ''and'')\\
 & {\tt ~~$\langle$OR$\rangle$ |} & disjunction (logical ''or'')\\
 & {\tt ~~$\langle$IMPL$\rangle$ |} & implication\\
 & {\tt ~~$\langle$EQUI$\rangle$ |} & logical equivalence\\
 & {\tt ~~$\langle$PREDVAR$\rangle$ |} & predicate variable\\
 & {\tt ~~$\langle$FORALL$\rangle$ |} & universal quantifier\\
 & {\tt ~~$\langle$EXISTS$\rangle$ |} & existential quantifier\\
 & {\tt ~~$\langle$FPATTERN$\rangle$ |} & pattern variable which can stand for any formula (used for abbreviations)\\
 & {\tt ~~$\langle$SPATTERN$\rangle$} & pattern variable which can stand for any predicate variable (used for abbreviations)\\
  &  {\tt ~)} & or list\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PROP$\rangle$} & & proposition variable\\
{\tt ~~$::=$~'PROP('} & \\
 & {\tt ~$\langle$number$\rangle$} & identification number\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$number$\rangle$} & & numeric atom, an integer\\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$NOT$\rangle$} & & negation\\
{\tt ~~$::=$~'NOT('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$} & formula to negate\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$AND$\rangle$} & & conjunction (logical ''and'')\\
{\tt ~~$::=$~'AND('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$,} & first argument\\
 & {\tt ~$\langle$FORMULA$\rangle$} & second argument\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$OR$\rangle$} & & disjunction (logical ''or'')\\
{\tt ~~$::=$~'OR('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$,} & first argument\\
 & {\tt ~$\langle$FORMULA$\rangle$} & second argument\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$IMPL$\rangle$} & & logical implication\\
{\tt ~~$::=$~'IMPL('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$,} & first formula\\
 & {\tt ~$\langle$FORMULA$\rangle$} & second formula\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$EQUI$\rangle$} & & logical equivalence\\
{\tt ~~$::=$~'EQUI('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$,} & formula\\
 & {\tt ~$\langle$FORMULA$\rangle$} & formula\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PREDVAR$\rangle$} & & predicate variable\\
{\tt ~~$::=$~'PREDVAR('} & \\
 & {\tt ~$\langle$number$\rangle$,} & identification number\\
 & {\tt ~$\langle$L$\rangle$} & list of subject variables\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$L$\rangle$} & & list of subject variables\\
{\tt ~~$::=$~'L('} & \\
 & {\tt ~\{$\langle$VAR$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$VAR$\rangle$} & & subject variable\\
{\tt ~~$::=$~'VAR('} & \\
 & {\tt ~$\langle$number$\rangle$} & identification number\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$FORALL$\rangle$} & & universal quantifier\\
{\tt ~~$::=$~'FORALL('} & \\
 & {\tt ~$\langle$VAR$\rangle$,} & quantify over this subject variable\\
 & {\tt ~$\langle$FORMULA$\rangle$} & formula which has the above subject variable as a free variable\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$EXISTS$\rangle$} & & existential quantifier\\
{\tt ~~$::=$~'EXISTS('} & \\
 & {\tt ~$\langle$VAR$\rangle$,} & quantify over this subject variable\\
 & {\tt ~$\langle$FORMULA$\rangle$} & formula which has the above subject variable as a free variable\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$FPATTERN$\rangle$} & & formula pattern variable\\
{\tt ~~$::=$~'FPATTERN('} & \\
 & {\tt ~$\langle$number$\rangle$} & identification number\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$SPATTERN$\rangle$} & & subject variable pattern variable\\
{\tt ~~$::=$~'SPATTERN('} & \\
 & {\tt ~$\langle$number$\rangle$} & identification number\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$AXIOM$\rangle$} & & declaration of an axiom, that is a stressed formula\\
{\tt ~~$::=$~'AXIOM('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$} & axiom formula\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$DECLARERULE$\rangle$} & & declaration of a new rule\\
{\tt ~~$::=$~'DECLARERULE('} & \\
 & {\tt ~$\langle$text$\rangle$,} & rule name\\
 & {\tt ~$\langle$text$\rangle$,} & rule description\\
 & {\tt ~\{$\langle$LINK$\rangle$\}} & references to  necessary axioms, propositions\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$LINK$\rangle$} & & rererences to a label of an axiom, proposition\\
{\tt ~~$::=$~'LINK('} & \\
 & {\tt ~$\langle$text$\rangle$} & label name\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PROPOSITION$\rangle$} & & consists of a mathematical theorem and its proof\\
{\tt ~~$::=$~'PROPOSITION('} & \\
 & {\tt ~$\langle$SENTENCE$\rangle$,} & theorem\\
 & {\tt ~$\langle$PROOF$\rangle$} & proof, last proof formula must be identical to theorem\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$SENTENCE$\rangle$} & & mathematical theorem\\
{\tt ~~$::=$~'SENTENCE('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$} & true mathematical formula\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PROOF$\rangle$} & & proof of a mathematical theorem, consists sequent proof lines, each one is constructed by using logical rules by foregoing proof lines, axioms, abbreviations or propositions\\
{\tt ~~$::=$~'PROOF('} & \\
 & {\tt ~$\langle$LINE$\rangle$,} & proof lines\\
 & {\tt ~\{$\langle$LINE$\rangle$\}} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$LINE$\rangle$} & & single proof line, consists of a derived formula and an information about the used rule and necessary references that enable the derivation\\
{\tt ~~$::=$~'LINE('} & \\
 & {\tt ~$\langle$FORMULA$\rangle$,} & \\
 & {\tt ~( } & \\
 & {\tt ~~$\langle$ADDAXIOM$\rangle$ |} & simple addition of an axiom to the prooflines\\
 & {\tt ~~$\langle$ADDSENTENCE$\rangle$ |} & simple addition of an already proved proposition\\
 & {\tt ~~$\langle$MODUSPONENS$\rangle$ |} & execution of Modus Ponens\\
 & {\tt ~~$\langle$REPLACEPROP$\rangle$ |} & replacement of an propositional variable\\
 & {\tt ~~$\langle$USEABBREVIATION$\rangle$ |} & usage of an abbreviation\\
 & {\tt ~~$\langle$REVERSEABBREVIATION$\rangle$ |} & reverse an abbreviation\\
 & {\tt ~~$\langle$RENAMEFREEVARIABLE$\rangle$ |} & rename a free subject variable\\
 & {\tt ~~$\langle$RENAMEBOUNDVARIABLE$\rangle$ |} & rename a bound subject variable\\
 & {\tt ~~$\langle$REPLACEPREDICATE$\rangle$ |} & replace a predicate variable by a formula\\
 & {\tt ~~$\langle$GENERALIZATION$\rangle$ |} & execution of generalization\\
 & {\tt ~~$\langle$PARTICULARIZATION$\rangle$} & execution of particularization\\
  &  {\tt ~)} & or list\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$ADDAXIOM$\rangle$} & & add an axiom\\
{\tt ~~$::=$~'ADDAXIOM('} & \\
 & {\tt ~$\langle$LINK$\rangle$} & axiom reference\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$ADDSENTENCE$\rangle$} & & add an already proven proposition\\
{\tt ~~$::=$~'ADDSENTENCE('} & \\
 & {\tt ~$\langle$LINK$\rangle$} & \\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$MODUSPONENS$\rangle$} & & Modus Ponens\\
{\tt ~~$::=$~'MODUSPONENS('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number which references formula A\\
 & {\tt ~$\langle$number$\rangle$} & proof line number which references formula A -> B\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$REPLACEPROP$\rangle$} & & propositional variable replacement\\
{\tt ~~$::=$~'REPLACEPROP('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed\\
 & {\tt ~$\langle$PROP$\rangle$,} & this propositional variable should be replaced\\
 & {\tt ~$\langle$FORMULA$\rangle$} & replacement\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$USEABBREVIATION$\rangle$} & & use definition of an abbreviation\\
{\tt ~~$::=$~'USEABBREVIATION('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed\\
 & {\tt ~$\langle$LINK$\rangle$,} & abbreviation reference\\
 & {\tt ~$\langle$number$\rangle$} & this occurrence number of the abbreviation shall be transformed\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$REVERSEABBREVIATION$\rangle$} & & reverse definition of an abbreviation\\
{\tt ~~$::=$~'REVERSEABBREVIATION('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed\\
 & {\tt ~$\langle$LINK$\rangle$,} & abbreviation reference\\
 & {\tt ~$\langle$number$\rangle$} & this occurrence number of the abbreviation pattern shall be replaced by the abbreviation\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$RENAMEFREEVARIABLE$\rangle$} & & rename of a free subject variable\\
{\tt ~~$::=$~'RENAMEFREEVARIABLE('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed\\
 & {\tt ~$\langle$VAR$\rangle$,} & rename this free subject variable\\
 & {\tt ~$\langle$VAR$\rangle$} & with this (non bound) subject variable\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$RENAMEBOUNDVARIABLE$\rangle$} & & rename of a bound subject variable (at a specific location)\\
{\tt ~~$::=$~'RENAMEBOUNDVARIABLE('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed\\
 & {\tt ~$\langle$VAR$\rangle$,} & rename this bound subject variable\\
 & {\tt ~$\langle$VAR$\rangle$,} & with this (non free) subject variable, which thereby must not get bound a second time\\
 & {\tt ~$\langle$number$\rangle$} & this occurrence of an quantor with the designated subject variable shall be target of the operation\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$REPLACEPREDICATE$\rangle$} & & replace predicate by formula\\
{\tt ~~$::=$~'REPLACEPREDICATE('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed\\
 & {\tt ~$\langle$PREDVAR$\rangle$,} & with pairwise different pattern variables as arguments\\
 & {\tt ~$\langle$FORMULA$\rangle$} & formular which contains the same pattern variables, the set of free subject variables must be disjunct to the set of bounded subject variables of the referenced proof line and conversely (the set of bounded subject variables must be disjunct to the set of free subject variables of the referenced proof line) and the predicate variable must not occur in the sphere of action of an quantor with an associated subject variable that is also contained in this formula\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$GENERALIZATION$\rangle$} & & generalization rule\\
{\tt ~~$::=$~'GENERALIZATION('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed, must have the form A -> B(x), with x not contained in A\\
 & {\tt ~$\langle$VAR$\rangle$} & this subject variable is generalized\\
{\tt ~~~~~~')';} & & \\
\end{longtable}

\begin{longtable}[h!]{@{\extracolsep{\fill}}p{1cm}@{\extracolsep{\fill}}p{4.5cm}@{\extracolsep{\fill}}p{8.5cm}}
  {\bf $\langle$PARTICULARIZATION$\rangle$} & & particularization rule\\
{\tt ~~$::=$~'PARTICULARIZATION('} & \\
 & {\tt ~$\langle$number$\rangle$,} & proof line number at which the rule should be executed, must have the form A(x) -> B, with x not contained in B\\
 & {\tt ~$\langle$VAR$\rangle$} & this subject variable is particularized\\
{\tt ~~~~~~')';} & & \\
\end{longtable}


\end{document}