Commit 6b983337 authored by Michael Kohlhase's avatar Michael Kohlhase
Browse files

use case

parent 495890c3
......@@ -10,13 +10,17 @@
\usepackage{mdframed}
\usepackage{wrapfig}
\usepackage{paralist}
\usepackage{xspace}
%\usepackage{appendix}
\usepackage[style=alphabetic,hyperref=auto,defernumbers=true,backend=bibtex,firstinits=true,maxbibnames=9,maxcitenames=3,isbn=false]{biblatex}
% \addbibresource{../../fr-macros/rabe.bib}
% \addbibresource{../../fr-macros/systems.bib}
% \addbibresource{../../fr-macros/pub_rabe.bib}
% \addbibresource{../../kwarc.bib}
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
\renewbibmacro*{event+venue+date}{}
\renewbibmacro*{doi+eprint+url}{%
\iftoggle{bbx:doi}
......@@ -34,7 +38,8 @@
\setlength{\hfuzz}{3pt} \hbadness=10001
\setcounter{tocdepth}{2} % for pdf bookmarks
\usepackage{xcolor}
\usepackage{listings}
\lstset{columns=fullflexible,basicstyle=\sf}
\usepackage[bookmarks,linkcolor=red,citecolor=blue,urlcolor=gray,colorlinks,breaklinks,bookmarksopen,bookmarksnumbered]{hyperref}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
......@@ -44,7 +49,11 @@
% \usepackage[llncs]{../../fr-macros/theorems}
% \input{macros}
\usepackage[hide]{ed}
\def\cB{\mathcal{B}}
\def\cL{\mathcal{L}}
\def\defemph{\textbf}
\def\MMT{\textsf{MMT}\xspace}
\usepackage[show]{ed}
\newif\ifshort\shorttrue
\pagestyle{plain} % remove for final version
......@@ -68,12 +77,79 @@
\section{Applications}\label{sec:appl}
\subsection{Theory Classification}\label{sec:classifier}
``Semantic Search'' -- a very suggestive term, which is alas seriously under-defined --
has often been touted as the ``killer application'' of semantic technologies. With a view
finder, we can add another possible interpretation: searching mathematical ontologies
(here modular theorem prover libraries) at the level of theories -- we call this \defemph{theory
classification}.
The basic use case is the following: Jane, a mathematician, becomes interested in a class
of mathematical objects, say -- as a didactic example -- something she initially calls
``beautiful subsets'' of a base set $\cB$ (or just ``beautiful over $\cB$''). These have
the following properties:
\begin{compactenum}
\item the empty set is beautiful over $\cB$
\item every subset of a beautiful set is beautiful over $\cB$
\item If $A$ and $B$ are beautiful over $\cB$and $A$ has more elements than $B$, then
there is an $x\in A\backslash B$, such that $B\cup\{x\}$ is beautiful over $\cB$.
\end{compactenum}
To see what is known about beautiful sets, she types these three conditions into a theory
classifier, which interprets them as a \MMT theory $Q$, computes all (total) views from
$Q$ into a library $\cL$, and returns presentations of target theories and the assignments
made by the views. In our example we have the situation in
Figure~\ref{fig:theory-classification-ex}\ednote{MK: Maybe better do this in jEdit and use
screenshots} \ednote{Interesting: the $\emptyset$ clause could also be ``$\exists S$
beautiful'', which is equivalent via the subset clause, maybe use that in the example:
define Matroid with that and have a theorem that says that $\emptyset$ is beautiful. Just
see what the viewfinder catches.} In the base use case, Jane learns that her
``beautiful sets'' correspond to the well-known structure of
matroids~\cite{wikipedia:matroid}, so she can directly apply matroid theory to her
problems.
\begin{newpart}{MK: this could/should be extended}
In extended use cases, we could
\begin{compactitem}
\item use partial views to find theories that share significant structure with $Q$, so
that we can formalize $Q$ with modularly with minimal effort. Say Jane was interested in
``dazzling subsets'', i.e. beautiful subsets that obey a fourth condition, then she
could just contribute a theory that extends \textsf{matroid} by a formalization of the
fourth condition -- and maybe rethink the name.
\item use existing views in $\cL$ (compositions of views are vivews) to give Jane more
information about her beautiful subsets, e.g. that matroids (and thus beautiful sets)
form a generalization of the notion of linear independence from linear algebra.
\end{compactitem}
\end{newpart}
\begin{figure}[ht]\centering\lstset{aboveskip=0pt,belowskip=0pt}
\begin{tabular}{|p{5cm}|p{5cm}|}\hline
$Q$ & Result \\\hline
\begin{lstlisting}[mathescape]
theory query : F?MitM
include ?set
Base : {A} set A
beautiful {A} set A $\rightarrow$ prop
empty : $\vdash$ beautiful $\emptyset$
subset-closed: $\vdash$ {}
\end{lstlisting}
&
\begin{lstlisting}[mathescape]
theory matroid : F?MitM
include ?baseset
independent {A} set A $\rightarrow$
empty: $\vdash$
hereditary : $\vdash$
augmentation: $\vdash$
\end{lstlisting}
\\\hline
\end{tabular}
\caption{Theory Classification for beautiful sets}\label{fig:theory-classification-ex}
\end{figure}
\section{Conclusion}\label{sec:concl}
\subsubsection*{Acknowledgements}
The authors gratefully acknowledge financial support from the OpenDreamKit Horizon 2020
European Research Infrastructures project (\#676541) and the DFG-funded projec OAF: An
European Research Infrastructures project (\#676541) and the DFG-funded project OAF: An
Open Archive for Formalizations (KO 2428/13-1).
\renewcommand*{\bibfont}{\small}
......@@ -89,4 +165,7 @@ Open Archive for Formalizations (KO 2428/13-1).
% LocalWords: inst maketitle formalization defs well-formedness textsf sec:impl impl
% LocalWords: sec:conc conc Universit printbibliography ednote Internalizing newpage
% LocalWords: ifshort sec:relwork relwork renewcommand bibfont
% LocalWords: ifshort sec:relwork relwork renewcommand bibfont tbw setcounter tocdepth
% LocalWords: tableofcontents defemph compactenum emptyset newpart compactitem lstset
% LocalWords: centering aboveskip 0pt,belowskip hline lstlisting mathescape rightarrow
% LocalWords: vdash baseset sec:concl subsubsection Formalizations
Supports Markdown
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