Attention: Maintenance on monday 19.04.2021 from 07:00 - 13:00 (Gitlab and Mattermost are offline!)

Commit de3e97a7 authored by Michael Kohlhase's avatar Michael Kohlhase

more grammar, and note

parent 138ac7ea
......@@ -4,4 +4,5 @@ fun
prime_A : A ;
integer_N : N ;
call_V2 : V2;
iff_Subj : Subj;
}
......@@ -11,4 +11,5 @@ lin
prime_A = regADeg "prime" ;
integer_N = regN "integer" ;
call_V2 = dirV2 (regV "call") ;
iff_Subj = mkSubj "iff";
}
......@@ -4,7 +4,7 @@
\usepackage{stex-logo}
\usepackage{listings}
\lstset{language=TeX,basicstyle=\sf}
\lstset{language=TeX,basicstyle=\sf,columns=fullflexible}
\lstdefinelanguage{GF}{
morekeywords={ abstract, concrete, resource, interface, instance,
incomplete, of, with, open,
......@@ -150,10 +150,21 @@ To understand the problem better, we consider the following example sentence:
We would like to parse this sentence with \GF (\lstinline[language={}]{p -cat=EN})
and linearize it into \mmt (\lstinline[language={}]{l -cat=MMT}):
$$\forall m:\mathbb{N}.\texttt{prime}(n) \Leftrightarrow
\nexists m : \mathbb{N}. 1 < m < n \land m \divides n$$
\[\forall m:\mathbb{N}.\texttt{prime}(n) \Leftrightarrow
\nexists m : \mathbb{N}. 1 < m < n \land m \divides n\]
\section{Question: How to use \GF for Formulae}
or something logically equivalent.
We have started a grammar \lstinline|Math.gf|/\lstinline|MathEng.gf| which can partially
do that. Here are some limitations and problems: What to do about
\begin{enumerate}
\item \nlex{an integer $n$}, i.e. apposition-like things.
\item \nlex{is called prime} this may be a math idiom.
\item \nlex{$A$, iff $B$} and \nlex{$A$, if $B$}; the whole handling of if does not seem
to work in the underlying grammar from the GF distribution.
\end{enumerate}
\section{Question: How to use \GF for Formulae}\label{sec:formulae}
\ednote{I do not know yet}
The \GF already has the math grammars from the WebAlt and Molto projects~\cite{MOLTO:on},
......@@ -173,7 +184,9 @@ in~\cite{SalXam:tgml12,CaprottiSaludes:OpenMathUIWiP2012,ArcCapRanSal:ugmam12}
% LocalWords: maketitle smglom setcounter tocdepth tableofcontents newpage textbf tbw
% LocalWords: Ranta:GF04,ranta-2011,GF:on linearizations Kofler:dgpnml17 Pichler:srmk16
% LocalWords: Humayoun's HumayounMNMTCNL,MathNat:on,Humayoun:phd CMLgrammar:on
% LocalWords: Wagner:coamas10,WAB:PAMbTEaPAS,AutexierEtAl:notations-texmacs-plato
% LocalWords: molto-gf:on sec:concl printbibliography
% LocalWords: Humayoun's HumayounMNMTCNL,MathNat:on,Humayoun:phd CMLgrammar:on mmt emph
% LocalWords: Wagner:coamas10,WAB:PAMbTEaPAS,AutexierEtAl:notations-texmacs-plato nlex
% LocalWords: molto-gf:on sec:concl printbibliography Ranta:tlled11 emptyset lstinline
% LocalWords: SalXam:tgml12,CaprottiSaludes:OpenMathUIWiP2012,ArcCapRanSal:ugmam12
% LocalWords: emptyset.gf lstinputlisting oneWordExample.gf oneWordExampleEN.gf forall
% LocalWords: mathbb Leftrightarrow nexists Math.gf MathEng.gf
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