Commit 50fd7223 authored by Michael Kohlhase's avatar Michael Kohlhase

adding

parent 642c29c4
\begin{module}[id=grader]
\symdef{grader}{\text{\texttt{JGrader}}}
\symdef{grader}{\operatorname{\texttt{JGrader}}}
\begin{frame}
\frametitle{Homework Submissions, Grading, Tutorials}
\begin{itemize}
......
\begin{module}[id=complexity-classes]
\symdef{PSPACE}{\text{PSPACE}}
\symdef{EXPTIME}{\text{EXPTIME}}
\symdef{PSPACE}{\operatorname{PSPACE}}
\symdef{EXPTIME}{\operatorname{EXPTIME}}
\end{module}
%%% Local Variables:
%%% mode: LaTeX
......
\begin{module}[id=complog-systems]
\symdef{loui}{\text{\ensuremath{\mathcal{L}\Omega\mathcal{UI}}}}
\symdef{inka}{\text{\texttt{InKa}}}
\symdef{otter}{\text{\texttt{Otter}}}
\symdef{spass}{\text{\texttt{Spass}}}
\symdef{tps}{\text{\texttt{TPS}}}
\symdef{protein}{\text{\texttt{ProTeIn}}}
\symdef{bliksem}{\text{\texttt{Bliksem}}}
\symdef{satchmo}{\text{\texttt{Satchmo}}}
\symdef{vampire}{\text{\texttt{Vampire}}}
\symdef{waldmeister}{\text{\texttt{WaldMeister}}}
\symdef{eprover}{\text{\texttt{EProver}}}
\symdef{tramp}{\text{\texttt{Tramp}}}
\symdef{mace}{\text{\texttt{Mace}}}
\symdef{kimba}{\text{\texttt{Kimba}}}
\symdef{sem}{\text{\texttt{Sem}}}
\symdef{OMEGA}{{\ensuremath\Omega}{\text{\texttt{mega}}}}
\symdef{loui}{\operatorname{\ensuremath{\mathcal{L}\Omega\mathcal{UI}}}}
\symdef{inka}{\operatorname{\texttt{InKa}}}
\symdef{otter}{\operatorname{\texttt{Otter}}}
\symdef{spass}{\operatorname{\texttt{Spass}}}
\symdef{tps}{\operatorname{\texttt{TPS}}}
\symdef{protein}{\operatorname{\texttt{ProTeIn}}}
\symdef{bliksem}{\operatorname{\texttt{Bliksem}}}
\symdef{satchmo}{\operatorname{\texttt{Satchmo}}}
\symdef{vampire}{\operatorname{\texttt{Vampire}}}
\symdef{waldmeister}{\operatorname{\texttt{WaldMeister}}}
\symdef{eprover}{\operatorname{\texttt{EProver}}}
\symdef{tramp}{\operatorname{\texttt{Tramp}}}
\symdef{mace}{\operatorname{\texttt{Mace}}}
\symdef{kimba}{\operatorname{\texttt{Kimba}}}
\symdef{sem}{\operatorname{\texttt{Sem}}}
\symdef{OMEGA}{{\ensuremath\Omega}{\operatorname{\texttt{mega}}}}
\symdef{leo}{\ensuremath\mathcal{LEO}}
\symdef{maple}{\text{\texttt{Maple}}}
\symdef{magma}{\text{\texttt{MagMa}}}
\symdef{gap}{\text{\texttt{Gap}}}
\symdef{maple}{\operatorname{\texttt{Maple}}}
\symdef{magma}{\operatorname{\texttt{MagMa}}}
\symdef{gap}{\operatorname{\texttt{Gap}}}
\symdef{cosie}{\ensuremath{\mathcal{C}o\mathcal{SIE}}}
\symdef{chorus}{\text{\texttt{Chorus}}}
\symdef{rdl}{\text{\texttt{RDL}}}
\symdef{hr}{\text{\texttt{HR}}}
\symdef{lambdaclam}{{\ensuremath\lambda}{\text{\texttt{Clam}}}}
\symdef{imps}{\text{\texttt{Imps}}}
\symdef{pvs}{\text{\texttt{Pvs}}}
\symdef{coq}{\text{\texttt{Coq}}}
\symdef{automath}{\text{\texttt{AutoMath}}}
\symdef{casl}{{\text{\texttt{Casl}}}}
\symdef{chorus}{\operatorname{\texttt{Chorus}}}
\symdef{rdl}{\operatorname{\texttt{RDL}}}
\symdef{hr}{\operatorname{\texttt{HR}}}
\symdef{lambdaclam}{{\ensuremath\lambda}{\operatorname{\texttt{Clam}}}}
\symdef{imps}{\operatorname{\texttt{Imps}}}
\symdef{pvs}{\operatorname{\texttt{Pvs}}}
\symdef{coq}{\operatorname{\texttt{Coq}}}
\symdef{automath}{\operatorname{\texttt{AutoMath}}}
\symdef{casl}{{\operatorname{\texttt{Casl}}}}
\begin{frame}
\frametitle{Computational Logic Systems}
......
\begin{module}[id=editors] % general Editors, presupposed
\symdef{emacsEditor}{\text{\texttt{emacs}}}
\symdef{viEditor}{\text{\texttt{vi}}}
\symdef{MSWord}{\text{\texttt{MS Word}}}
\symdef{emacsEditor}{\operatorname{\texttt{emacs}}}
\symdef{viEditor}{\operatorname{\texttt{vi}}}
\symdef{MSWord}{\operatorname{\texttt{MS Word}}}
\end{module}
%%% Local Variables:
......
\begin{module}[id=gregorian]
\symdef{gregorianADOp}{\text{AD}}
\symdef{gregorianADOp}{\operatorname{AD}}
\symdef{gregorianADdate}[3]{\mixfixiii[nobrackets]{}{#1}{.\;}{#2}{.\;}{#3}\gregorianADOp}
\symdef{gregorianADmonth}[2]{\mixfixii[nobrackets]{}{#1}{.\;}{#2}\gregorianADOp}
\symdef{gregorianADyear}[1]{\mixfixi[nobrackets]{}{#1}\gregorianADOp}
\symdef{gregorianBCOp}{\text{BC}}
\symdef{gregorianBCOp}{\operatorname{BC}}
\symdef{gregorianBCdate}[3]{\mixfixiii[nobrackets]{}{#1}{.\;}{#2}{.\;}{#3}\gregorianBCOp}
\symdef{gregorianBCmonth}[2]{\mixfixii[nobrackets]{}{#1}{.\;}{#2}\gregorianBCOp}
\symdef{gregorianBCyear}[1]{\mixfixi[nobrackets]{}{#1}\gregorianBCOp}
......
\begin{module}[id=operatingsystems] % general operating systems, presupposed
\symdef{unixOS}{\text{\texttt{UNIX}}}
\symdef{linuxOS}{\text{\texttt{linux}}}
\symdef{macosxOS}{\text{\texttt{Mac OS X}}}
\symdef{cygwinOS}{\text{\texttt{cygwin}}}
\symdef{windowsOS}{\text{\texttt{Windows}}}
\symdef{unixOS}{\operatorname{\texttt{UNIX}}}
\symdef{linuxOS}{\operatorname{\texttt{linux}}}
\symdef{macosxOS}{\operatorname{\texttt{Mac OS X}}}
\symdef{cygwinOS}{\operatorname{\texttt{cygwin}}}
\symdef{windowsOS}{\operatorname{\texttt{Windows}}}
\end{module}
%%% Local Variables:
......
\begin{module}[id=proglang] % general Programming languages, presupposed
\symdef{CLanguage}{\text{\texttt{C}}}
\symdef{CppLanguage}{\text{\texttt{C}}^{\text{\texttt{++}}}}
\symdef{JavaLanguage}{{\text{\texttt{Java}}}}
\symdef{SMLLanguage}{\text{\texttt{SML}}}
\symdef{mozartLanguage}{{\text{\texttt{mOZart}}}}
\symdef{OZLanguage}{{\text{\texttt{OZ}}}}
\symdef{LISPLanguage}{{\text{\texttt{LISP}}}}
\symdef{FortranLanguage}{{\text{\texttt{FORTRAN}}}}
\symdef{CobolLanguage}{{\text{\texttt{COBOL}}}}
\symdef{CLanguage}{\operatorname{\texttt{C}}}
\symdef{CppLanguage}{\operatorname{\texttt{C}}^{\operatorname{\texttt{++}}}}
\symdef{JavaLanguage}{{\operatorname{\texttt{Java}}}}
\symdef{SMLLanguage}{\operatorname{\texttt{SML}}}
\symdef{mozartLanguage}{{\operatorname{\texttt{mOZart}}}}
\symdef{OZLanguage}{{\operatorname{\texttt{OZ}}}}
\symdef{LISPLanguage}{{\operatorname{\texttt{LISP}}}}
\symdef{FortranLanguage}{{\operatorname{\texttt{FORTRAN}}}}
\symdef{CobolLanguage}{{\operatorname{\texttt{COBOL}}}}
\end{module}
%%% Local Variables:
......
\begin{module}[id=realworldsorts]
\importmhmodule[repos=MiKoMH/GenCS,path=logic/en/sorts-base]{sorts-base}
\abbrdef{explicitsort}[1]{\text{\texttt{#1}}}
\abbrdef{explicitsort}[1]{\operatorname{\texttt{#1}}}
\symdef{sortentity}{\sorte\explicitsort{ntity}}
\symdef{sortabstract}{\sorta\explicitsort{bstract}}
\symdef{sortreal}{\sortr\explicitsort{eal}}
......
\begin{module}[id=some-characters]
\symdef{achar}{\text{\texttt{a}}}
\symdef{bchar}{\text{\texttt{b}}}
\symdef{cchar}{\text{\texttt{c}}}
\symdef{dchar}{\text{\texttt{d}}}
\symdef{echar}{\text{\texttt{e}}}
\symdef{fchar}{\text{\texttt{f}}}
\symdef{gchar}{\text{\texttt{g}}}
\symdef{hchar}{\text{\texttt{h}}}
\symdef{ichar}{\text{\texttt{i}}}
\symdef{jchar}{\text{\texttt{j}}}
\symdef{kchar}{\text{\texttt{k}}}
\symdef{lchar}{\text{\texttt{l}}}
\symdef{mchar}{\text{\texttt{m}}}
\symdef{nchar}{\text{\texttt{n}}}
\symdef{ochar}{\text{\texttt{o}}}
\symdef{pchar}{\text{\texttt{p}}}
\symdef{qchar}{\text{\texttt{q}}}
\symdef{rchar}{\text{\texttt{r}}}
\symdef{schar}{\text{\texttt{s}}}
\symdef{tchar}{\text{\texttt{t}}}
\symdef{uchar}{\text{\texttt{u}}}
\symdef{vchar}{\text{\texttt{v}}}
\symdef{wchar}{\text{\texttt{w}}}
\symdef{xchar}{\text{\texttt{x}}}
\symdef{ychar}{\text{\texttt{x}}}
\symdef{zchar}{\text{\texttt{z}}}
\symdef{achar}{\operatorname{\texttt{a}}}
\symdef{bchar}{\operatorname{\texttt{b}}}
\symdef{cchar}{\operatorname{\texttt{c}}}
\symdef{dchar}{\operatorname{\texttt{d}}}
\symdef{echar}{\operatorname{\texttt{e}}}
\symdef{fchar}{\operatorname{\texttt{f}}}
\symdef{gchar}{\operatorname{\texttt{g}}}
\symdef{hchar}{\operatorname{\texttt{h}}}
\symdef{ichar}{\operatorname{\texttt{i}}}
\symdef{jchar}{\operatorname{\texttt{j}}}
\symdef{kchar}{\operatorname{\texttt{k}}}
\symdef{lchar}{\operatorname{\texttt{l}}}
\symdef{mchar}{\operatorname{\texttt{m}}}
\symdef{nchar}{\operatorname{\texttt{n}}}
\symdef{ochar}{\operatorname{\texttt{o}}}
\symdef{pchar}{\operatorname{\texttt{p}}}
\symdef{qchar}{\operatorname{\texttt{q}}}
\symdef{rchar}{\operatorname{\texttt{r}}}
\symdef{schar}{\operatorname{\texttt{s}}}
\symdef{tchar}{\operatorname{\texttt{t}}}
\symdef{uchar}{\operatorname{\texttt{u}}}
\symdef{vchar}{\operatorname{\texttt{v}}}
\symdef{wchar}{\operatorname{\texttt{w}}}
\symdef{xchar}{\operatorname{\texttt{x}}}
\symdef{ychar}{\operatorname{\texttt{x}}}
\symdef{zchar}{\operatorname{\texttt{z}}}
\symdef{Achar}{\text{\texttt{A}}}
\symdef{Bchar}{\text{\texttt{B}}}
\symdef{Cchar}{\text{\texttt{C}}}
\symdef{Dchar}{\text{\texttt{D}}}
\symdef{Echar}{\text{\texttt{E}}}
\symdef{Fchar}{\text{\texttt{F}}}
\symdef{Gchar}{\text{\texttt{G}}}
\symdef{Hchar}{\text{\texttt{H}}}
\symdef{Ichar}{\text{\texttt{I}}}
\symdef{Jchar}{\text{\texttt{J}}}
\symdef{Kchar}{\text{\texttt{K}}}
\symdef{Lchar}{\text{\texttt{L}}}
\symdef{Mchar}{\text{\texttt{M}}}
\symdef{Nchar}{\text{\texttt{N}}}
\symdef{Ochar}{\text{\texttt{O}}}
\symdef{Pchar}{\text{\texttt{P}}}
\symdef{Qchar}{\text{\texttt{Q}}}
\symdef{Rchar}{\text{\texttt{R}}}
\symdef{Schar}{\text{\texttt{S}}}
\symdef{Tchar}{\text{\texttt{T}}}
\symdef{Uchar}{\text{\texttt{U}}}
\symdef{Vchar}{\text{\texttt{V}}}
\symdef{Wchar}{\text{\texttt{W}}}
\symdef{Xchar}{\text{\texttt{X}}}
\symdef{Ychar}{\text{\texttt{X}}}
\symdef{Zchar}{\text{\texttt{Z}}}
\symdef{Achar}{\operatorname{\texttt{A}}}
\symdef{Bchar}{\operatorname{\texttt{B}}}
\symdef{Cchar}{\operatorname{\texttt{C}}}
\symdef{Dchar}{\operatorname{\texttt{D}}}
\symdef{Echar}{\operatorname{\texttt{E}}}
\symdef{Fchar}{\operatorname{\texttt{F}}}
\symdef{Gchar}{\operatorname{\texttt{G}}}
\symdef{Hchar}{\operatorname{\texttt{H}}}
\symdef{Ichar}{\operatorname{\texttt{I}}}
\symdef{Jchar}{\operatorname{\texttt{J}}}
\symdef{Kchar}{\operatorname{\texttt{K}}}
\symdef{Lchar}{\operatorname{\texttt{L}}}
\symdef{Mchar}{\operatorname{\texttt{M}}}
\symdef{Nchar}{\operatorname{\texttt{N}}}
\symdef{Ochar}{\operatorname{\texttt{O}}}
\symdef{Pchar}{\operatorname{\texttt{P}}}
\symdef{Qchar}{\operatorname{\texttt{Q}}}
\symdef{Rchar}{\operatorname{\texttt{R}}}
\symdef{Schar}{\operatorname{\texttt{S}}}
\symdef{Tchar}{\operatorname{\texttt{T}}}
\symdef{Uchar}{\operatorname{\texttt{U}}}
\symdef{Vchar}{\operatorname{\texttt{V}}}
\symdef{Wchar}{\operatorname{\texttt{W}}}
\symdef{Xchar}{\operatorname{\texttt{X}}}
\symdef{Ychar}{\operatorname{\texttt{X}}}
\symdef{Zchar}{\operatorname{\texttt{Z}}}
\symdef{zerochar}{\text{\texttt{0}}}
\symdef{onechar}{\text{\texttt{1}}}
\symdef{twochar}{\text{\texttt{2}}}
\symdef{threechar}{\text{\texttt{3}}}
\symdef{fourchar}{\text{\texttt{4}}}
\symdef{fivechar}{\text{\texttt{5}}}
\symdef{sixchar}{\text{\texttt{6}}}
\symdef{sevenchar}{\text{\texttt{7}}}
\symdef{eightchar}{\text{\texttt{8}}}
\symdef{ninechar}{\text{\texttt{9}}}
\symdef{slashchar}{\text{\texttt{/}}}
\symdef{hashchar}{\text{\texttt{\#}}}
\symdef{starchar}{\text{\texttt{*}}}
\symdef{dotchar}{\text{\texttt{.}}}
\symdef{obrackchar}{\text{\texttt{(}}}
\symdef{cbrackchar}{\text{\texttt{)}}}
\symdef{commachar}{\text{\texttt{,}}}
\symdef{pluschar}{\text{\texttt{+}}}
\symdef{minuschar}{\text{\texttt{-}}}
\symdef{zerochar}{\operatorname{\texttt{0}}}
\symdef{onechar}{\operatorname{\texttt{1}}}
\symdef{twochar}{\operatorname{\texttt{2}}}
\symdef{threechar}{\operatorname{\texttt{3}}}
\symdef{fourchar}{\operatorname{\texttt{4}}}
\symdef{fivechar}{\operatorname{\texttt{5}}}
\symdef{sixchar}{\operatorname{\texttt{6}}}
\symdef{sevenchar}{\operatorname{\texttt{7}}}
\symdef{eightchar}{\operatorname{\texttt{8}}}
\symdef{ninechar}{\operatorname{\texttt{9}}}
\symdef{slashchar}{\operatorname{\texttt{/}}}
\symdef{hashchar}{\operatorname{\texttt{\#}}}
\symdef{starchar}{\operatorname{\texttt{*}}}
\symdef{dotchar}{\operatorname{\texttt{.}}}
\symdef{obrackchar}{\operatorname{\texttt{(}}}
\symdef{cbrackchar}{\operatorname{\texttt{)}}}
\symdef{commachar}{\operatorname{\texttt{,}}}
\symdef{pluschar}{\operatorname{\texttt{+}}}
\symdef{minuschar}{\operatorname{\texttt{-}}}
\end{module}
%%% Local Variables:
%%% mode: LaTeX
......
\begin{module}[id=systems] % we have not introduced these
\abbrdef{scsys}[1]{\text{\texttt{#1}}}
\abbrdef{scsys}[1]{\operatorname{\texttt{#1}}}
\symdef{systemname}[1]{\mathop{#1}}
\symdef{EMACSEditor}{\text{\texttt{emacs}}}
\symdef{PUTTY}{\text{\texttt{putty}}}
\symdef{EMACSEditor}{\operatorname{\texttt{emacs}}}
\symdef{PUTTY}{\operatorname{\texttt{putty}}}
\symdef{Coq}{\scsys{Coq}}
\symdef{google}{\text{Google}}
\symdef{google}{\operatorname{Google}}
\symdef{MSexcel}{\text{MS Excel}}
\symdef{OOcalc}{\text{OO Calc}}
\symdef{OOcalc}{\operatorname{OO Calc}}
\symdef{AppleNumbers}{\text{Numbers}}
\symdef{gnuplot}{\text{gnuplot}}
\symdef{mathematica}{\text{\texttt{Mathematica}}}
\symdef{mysql}{\text{\texttt{MySQL}}}
\symdef{LAMPsystem}{\text{\texttt{LAMP}}}
\symdef{jdom}{\text{\texttt{JDOM}}}
\symdef{acrobatReader}{\text{\texttt{Acrobat Reader}}}
\symdef{acrobatDistiller}{\text{\texttt{Acrobat Distiller}}}
\symdef{pdf}{\text{\texttt{PDF}}}
\symdef{wordperfect}{\text{\texttt{WordPerfect}}}
\symdef{drupal}{\text{\texttt{Drupal}}}
\symdef{mathplayer}{\text{\texttt{MathPlayer}}}
\symdef{gnuplot}{\operatorname{gnuplot}}
\symdef{mathematica}{\text{\operatornamett{Mathematica}}}
\symdef{mysql}{\text{\operatornamett{MySQL}}}
\symdef{LAMPsystem}{\text{\operatornamett{LAMP}}}
\symdef{jdom}{\text{\operatornamett{JDOM}}}
\symdef{acrobatReader}{\text{\operatornamett{Acrobat Reader}}}
\symdef{acrobatDistiller}{\text{\operatornamett{Acrobat Distiller}}}
\symdef{pdf}{\text{\operatornamett{PDF}}}
\symdef{wordperfect}{\text{\operatornamett{WordPerfect}}}
\symdef{drupal}{\text{\operatornamett{Drupal}}}
\symdef{mathplayer}{\text{\operatornamett{MathPlayer}}}
\end{module}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment