slight re-arrangement of the examples:

the simple example becomes a cenelec example,
and simple got an example called Article based on
to the LNCS_onto.
This commit is contained in:
Burkhart Wolff 2018-04-04 16:14:37 +02:00
parent 5bc9ddfd52
commit 4d09fc5e34
2 changed files with 73 additions and 0 deletions

View File

@ -0,0 +1,73 @@
theory Article
imports "../../ontologies/LNCS_onto"
begin
text*[tit::title]{* Using The Isabelle Ontology Framework*}
text*[stit::subtitle] \<open>Linking the Formal with the Informal\<close>
text*[auth1::author, affiliation="Université Paris-Sud"]\<open>Burkhart Wolff\<close>
text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system
framework with many similarities to Eclipse; it is mostly known as part of
Isabelle/HOL, an interactive theorem proving and code generation
environment. Recently, an Document Ontology Framework has been
developed as a plugin in Isabelle/Isar, allowing to do both
conventional typesetting \emph{as well} as formal development.
A particular asset is the possibility to control the links
between the formal and informal aspects of a document
via (a novel use of) Isabelle's antiquotation mechanism.
*}
section*[intro::introduction, comment="''This is a comment''"]{* Introduction *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,
phasellus amet id massa nunc, pede suscipit repellendus, in ut tortor eleifend augue
pretium consectetuer. Lectus accumsan velit ultrices, mauris amet, id elit aliquam aptent id,
felis duis. Mattis molestie semper gravida in ullamcorper ut, id accumsan, fusce id
sed nibh ut lorem integer, maecenas sed mi purus non nunc, morbi pretium tortor.*}
section*[bgrnd::text_section]{* Background: Isabelle and Isabelle_DOF *}
text{* As mentioned in @{introduction \<open>intro\<close>} ... *}
section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*}
subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood. *}
subsection*[mathex_onto::example]{* Math-Exercise *}
subsection*[cenelec_onto::example]{* CENELEC *}
section*[con::conclusion]{* Future Work: Monitoring Classes *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ...
The control of monitors is done by the commands:
\<bullet> open_monitor <doc-class>
\<bullet> close_monitor <doc-class>
where the automaton of the monitor class is expected
to be in a final state.
Monitors can be nested, so it is possible to "overlay" one or more monitoring
classes and imposing different sets of structural constraints in a
Classes neither directly or via inheritance indirectly
mentioned in the monitor are @{bold \<open>nested\<close>}
from a monitor and may occur freely.
*}
subsection*[related::related_work]{* Related Work *}
text{*
\<bullet> XML and dtd's,
\<bullet> OWL and Protege,
\<bullet> LaTeX setups such as ...
@{url "https://pdi.fbk.eu/technologies/tex-owl-latex-style-syntax-authoring-owl-2-ontologies"}
\<bullet> Structured Assurance Case Metamodel Specification.
@{url "https://www.omg.org/spec/SACM/1.0/About-SACM/"}}
\<bullet> AADL Alisa,
\<bullet> RATP Ovado
*}
subsection{* Discussion *}
end