\documentclass[11pt,a4paper]{article}

\usepackage{latexsym}

\def\isac{${\cal I}\mkern-2mu{\cal S}\mkern-5mu{\cal AC}\:$}

\title{\isac Interfaces\\

        Frontend --- Kernel --- Frontend}

\author{Walther Neuper}

\begin{document}

\maketitle

\def\pow{\;\;\widehat{ }\;\;\widehat{ }\;\;\widehat{ }}

In the Backus-Naur-Form used below the symbols of the meta language

are $\; ::= \;\; | \;\; ( \;\; ) \;\; ^* \;\; ^+ \;\;\epsilon\;\;$ as usual, whereas

italic parenthesis {\it (} {\it )}, braces {\it\{} {\it\}} and

brackets {\it[} {\it]} belong to the object language. Terminal symbols

start with an upper-case letter (reminding of SML datatype

constructors), non-terminals start with a lower-case letter. The

nonterminals {\it int} and {\it string} are as defined in SML (in

particular: negative numbers are $\tilde{ }\,1,\cdots$ and not $-1,\cdots$, strings are quoted by ''$\;$''), {\it digit} has the obvious

meaning, and {\it MAT} is being defined elsewhere. Inserted comments {\it (* \dots *)} do not belong to the object-language.

\begin{tabbing}

123\={\it pro}\={\it ofID} \=cmd \=123\=123\=123\=123451234512345\=\kill

{\it FE-KE ::= }\\

\>\>$\:\;${\it StdinSML 0 0 0 0 New\_User ; cr}\\

\>\>$|\;${\it StdinSML userID 0 0 0 End\_User ; cr}\\

\>\>$|\;${\it StdinSML userID proofID acellID cellID dataFK ; cr}\\

\>{\it userID} \>\>::= {\it int}\\

\>{\it proofID}\>\>::= {\it int}\\

\>{\it acellID}\>\>::= {\it cellID}\\

\>{\it cellID} \>\>::= {\it int}\\

\>{\it cr} \>\>::= {\it carriage-return}\\

\\

\>{\it dataFK}\>\>::= {\it New\_Proof}  $\:|\:$ {\it End\_Proof}\\

\>\>\>$\:|\:$ {\it Command user\_cmd}\\

\>\>\>$\:|\:$ {\it RuleFK rule}\\

\>\>\>$\:|\:$ {\it FormFK MAT}\\

\>\>\>$\:|\:$ {\it PpcFK ( mat\_ppc} )\`\\

\\

\>\>{\it user\_cmd} ::= 

                {\it Accept} $\:|\:$ {\it NotAccept} $\:|\:$ {\it Example}\\

\>\>\>\>$\:|\:$ {\it YourTurn} $\:|\:$ {\it Rules} $\:|\:$ {\it DontKnow}\\

\>\>\>\>$\:|\:$ {\it Undo} $\:|\:$ {\it Auto} $\:|\:$ {\it Details}\`\\

\>\>\>\>$\:|\:$ {\it ActivePlus} $\:|\:$ {\it ActiveMinus}\`\\

\>\>\>\>$\:|\:$ {\it StepwidthPlus} $\:|\:$ {\it StepwidthMinus}\`\\

\\

\>\>{\it rule} ::= {\it Init\_Proof\_Hid ( dialogmode , mat\_list , spec )}\\

\>\>\>$|\:$ {\it Init\_Proof }\>\>\>\>\>$|\:$ {\it

Specify\_Domain domID} \\

\>\>\>$|\:$ {\it Specify\_Problem pblID}\>\>\>\>\>$|\:$ {\it

Specify\_Method metID} \\

\>\>\>$|\:$ {\it Add\_Given MAT}\>\>\>\>\>$|\:$ {\it Del\_Given MAT}\\

\>\>\>$|\:$ {\it Add\_Find MAT}\>\>\>\>\>$|\:$ {\it Del\_Find MAT}\\

\>\>\>$|\:$ {\it Add\_Relation MAT}\>\>\>\>\>$|\:$ {\it Del\_Relation MAT}\\

\>\>\>$|\:$ {\it Refine pblID}\>\>\>\>\>$|\:$ {\it Apply\_Method metID}\\

\>\>\>$|\:$ {\it Check\_Postcond pblID}\>\>\>\>\>$|\:$ {\it Free\_Solve}\\

\\    

\>\>\>$|\:$ {\it Rewrite\_Inst subs thm}

                              \>\>\>\>\>$|\:$ {\it Rewrite thm}\\

\>\>\>$|\:$ {\it Rewrite\_Set\_Inst ( subs , rls )}

                              \>\>\>\>\>$|\:$ {\it Rewrite\_Set rls}\`\\

\>\>\>$|\:$ {\it End\_Ruleset}\>\>\>\>\>$|\:$ {\it Calculate op}\\

\>\>\>$|\:$ {\it Rewrite\_Asm thm}\`\\

\\    

\>\>\>$|\:$ {\it Substitute subs}\>\>\>\>\>$|\:$ {\it Apply\_Assumption preds}\\

\>\>\>$|\:$ {\it Take term} \>\>\>\>\>$|\:$ {\it Take\_Inst term}\\

\>\>\>$|\:$ {\it Group ( con , int\_list )}\\

\>\>\>$|\:$ {\it Subproblem ( spec , mat\_list )}

                              \>\>\>\>\>$|\:$ {\it CAScmd term}\\

\\    

\>\>\>$|\:$ {\it Split\_And}  \>\>\>\>\>$|\:$ {\it Conclude\_And} \\

\>\>\>$|\:$ {\it Split\_Or}   \>\>\>\>\>$|\:$ {\it Conclude\_Or} \\

\>\>\>$|\:$ {\it Begin\_Trans}\>\>\>\>\>$|\:$ {\it End\_Trans} \\

\>\>\>$|\:$ {\it Begin\_Sequ} \>\>\>\>   \\

\>\>\>$|\:$ {\it Intersect}   \>\>\>\>\>$|\:$ {\it End\_Intersect} \\

\>\>\>$|\:$ {\it Check\_elementwise pred}

                             \>\>\>\>\>$|\:$ {\it Collect\_Trues}\`\\

\>\>\>$|\:$ {\it Mstep string}\\

\\

{\it mat\_ppc}::=

\>\>\>{\it ( ( Problem pblID )}$\:|\:${\it ( Method metID ))}\`\\ 

\>\>\>{\it Given  mat\_list}\\ 

\>\>\>{\it Where  mat\_list}\\ 

\>\>\>{\it Find   mat\_list}\\ 

\>\>\>{\it With   mat\_list}\\ 

\>\>\>{\it Relate mat\_list}\\

\\

{\it dialogmode} \>\>\>::= {\it string}\\

{\it domID} \>\>\>::= {\it string}\\

{\it pblID} \>\>\>::= {\it string\_list}\\

{\it metID} \>\>\>::= {\it ( domID , string )}\\

{\it spec}  \>\>\>::= {\it ( domID , pblID , metID )}\\

\\

{\it thm}  \>\>::= {\it ( thmID , MAT )}\>\>\>\>\>\>{\it (* theorem *)}\\

{\it thmID}\>\>::= {\it string}\\

{\it term} \>\>::= {\it MAT}\\

{\it pred} \>\>::= {\it MAT}\>\>\>\>\>\>     {\it (* predicate *)}\`\\

{\it preds}\>\>::= {\it mat\_list}\>\>\>\>\>\>{\it (* predicates *)}\\

{\it rls}  \>\>::= {\it string} \>\>\>\>\>\>{\it (* set of rewrite-rules *)}\\

{\it con}  \>\>::= {\it \&} $\:|\:$ {\it /}

                                  \>\>\>\>\>\>{\it (* }$\land,\lor${\it *)}\\

{\it op}   \>\>::= {\it''plus''} $\:|\:$ {\it''minus''} $\:|\:$ {\it''times''}\`\\

\>\>\hspace*{0.5em}$\:|\:$ {\it''cancel''} $\:|\:$ {\it''pow''} $\:|\:$ {\it''sqrt''}\`\\

{\it subs} \>\>::= {\it mat\_list}\>\>\>\>\>\>{\it (* substitutions as equalities *)}\\

\\

{\it int\_list} ::= \>\>\>\>{\it [} $\epsilon \:|\: ($ {\it int} $($

{\it , int} $)^*)$ {\it ]}\\

{\it string\_list} ::= \>\>\>\>{\it [} $\epsilon \:|\: ($ {\it string} $($

{\it , string} $)^*)$ {\it ]}\\

{\it mat\_list} ::= \>\>\>\>{\it [} $\epsilon \:|\: ($ {\it MAT} $($

{\it , MAT} $)^*)$ {\it ]}

\end{tabbing}

\newpage

\section{Interface Kernel --- Frontend}

%------------------------------------------------

\begin{tabbing}

123\={\it pro}\={\it ofID} \=cmd \=123\=123\=123\=12345123451234512345\=\kill {\it KE-FE ::= }\\

\>\>$\:\;${\it( userID , 0 , 0 , [$\,$] , New\_User )}\`(1)\\

\>\>$|\;${\it( userID , proofID , cellID , cellID\_list , dataKF\_list}\`(2)\\

\>{\it dataKF\_list} ::= {\it [ dataKF} $($

{\it , dataKF} $)^*$ {\it ]}\`(3)\\

\\

\>{\it dataKF} ::= {\it New\_Proof} $\:|\:$ {\it End\_Proof}\`(4)\\

\>\>\>$\:|\:$ {\it Request string} $\:|\:$ {\it Message

string} $\:|\:$ {\it Error string}\`(5)\\

\>\>\>$\:|\:$ {\it System string} $\:|\:$ {\it Indicate ind\_list}\`(6)\\

\>\>\>$\:|\:$ {\it Select [ rule} $($ {\it , rule} $)^*$ {\it ]}\`(7)\\

\>\>\>$\:|\:$ {\it Active int} $\:|\:$ {\it Speed int} $\:|\:$ {\it Domain domID}\`(8)\\

\\

\>\>\>$\:|\:$ {\it RuleKF ( edit , rule )}\`(9)\\

\\

\>\>\>$\:|\:$ {\it FormKF ( cellID , edit , indent , nest, MAT )}\`(10)\\

\>\>\>$\:|\:$ {\it PpcKF ( cellID , edit , indent , nest, tag\_ppc )}\`(11)\\

\\

\>\>{\it ind\_list}\>\> ::= {\it [ ind} $($ {\it , ind} $)^*$ {\it ]}\`(12)\\

\>\>\>{\it ind} \> ::= {\it ( ''guide'',} $($ {\it Safe} $\:|\:$ {\it Unsafe} $\:|\:$ {\it Helpless} $)$ {\it)}\`(13)\\

\>\>\>\>$\:|\:$ {\it ( ''proof'',} $($ {\it Incomplete} $\:|\:$ {\it Complete} $\:|\:$ {\it Inconsistent} $)$ {\it)}\`(14)\\ 

\>\>{\it edit}\>\> ::= {\it Write}$\:|\:${\it Protect}\`(15)\\

\>\>{\it indent}\>\> ::= {\it int}\`(16)\\

\>\>{\it nest}\>\> ::= {\it Open}$\:|\:${\it Closed}$\:|\:${\it Nundef}\`(17)\\

\>\>{\it tag\_ppc}\>\> ::= {\it (}\`(18)\\

\>\>\>\>\>( {\it Problem pblID}$\:|\:${\it Method metID} ) {\it,}\`(19)\\ 

\>\>\>\>\>\{ {\it Given  tag\_list ,}\`(20)\\ 

\>\>\>\>\>$\;$ {\it Where  tag\_list ,}\`(21)\\ 

\>\>\>\>\>$\;$ {\it Find   tag\_list ,}\`(22)\\ 

\>\>\>\>\>$\;$ {\it With   tag\_list ,}\`(23)\\ 

\>\>\>\>\>$\;$ {\it Relate tag\_list} \} {\it)}\`(24)\\

\>\>\>{\it tag\_list}\>\> ::= {\it [ tag MAT} $($ {\it , tag MAT} $)^*$ {\it ]}\`(25)\\

\>\>\>\>{\it tag}\>\> ::= {\it Correct}  $\:|\:$ {\it Superfl} $\:|\:$ {\it Incompl}\`(26)\\  

\>\>\>\>\>\>$\:|\:$ {\it False}  $\:|\:$ {\it Syntax}  $\:|\:$ {\it Type}\`(27)

\end{tabbing}

\end{document}