diff --git a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib index 2cc2d8da..a5c8f606 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib +++ b/examples/scholarly_paper/2021-ITP-PMTI/document/root.bib @@ -20,6 +20,44 @@ note = {Part of the Isabelle distribution.} } +@TechReport{Parsia:12:OWO, + author = "Bijan Parsia and Boris Motik and Peter Patel-Schneider", + title = "{OWL} 2 Web Ontology Language Structural Specification and Functional-Style Syntax (Second Edition)", + month = dec, + note = "https://www.w3.org/TR/2012/REC-owl2-syntax-20121211/", + year = "2012", + bibsource = "https://w2.syronex.com/jmr/w3c-biblio", + type = "{W3C} Recommendation", + institution = "W3C", +} + +@ARTICLE{1654194, + author={Brachman}, + journal={Computer}, + title={What IS-A Is and Isn't: An Analysis of Taxonomic Links in Semantic Networks}, + year={1983}, + volume={16}, + number={10}, + pages={30-36}, + doi={10.1109/MC.1983.1654194}} + +@article{DBLP:journals/corr/NevzorovaZKL14, + author = {Olga Nevzorova and + Nikita Zhiltsov and + Alexander Kirillovich and + Evgeny K. Lipachev}, + title = {{\textdollar}OntoMath{\^{}}\{PRO\}{\textdollar} Ontology: {A} Linked + Data Hub for Mathematics}, + journal = {CoRR}, + volume = {abs/1407.4833}, + year = {2014}, + url = {http://arxiv.org/abs/1407.4833}, + eprinttype = {arXiv}, + eprint = {1407.4833}, + timestamp = {Fri, 21 Aug 2020 16:53:16 +0200}, + biburl = {https://dblp.org/rec/journals/corr/NevzorovaZKL14.bib}, + bibsource = {dblp computer science bibliography, https://dblp.org} +} @TechReport{ bsi:50128:2014, type = {Standard}, diff --git a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy index 1cb7cfa7..e7d5a4dc 100644 --- a/examples/scholarly_paper/2021-ITP-PMTI/paper.thy +++ b/examples/scholarly_paper/2021-ITP-PMTI/paper.thy @@ -231,10 +231,10 @@ text\As novel contribution, this work extends prior versions of \<^dof> by \ text\ For example, the \<^dof> evaluation command taking a HOL-expression: @{theory_text [display,indent=6, margin=70] -\ value*[ass::Assertion, relvce=2::int] \mapfilter (\ \. relvce \ > 2) @{instance_of \Assertion\}\\ +\ value*[ass::Assertion, relvce=2::int] \filter (\ \. relvce \ > 2) @{Assertion-instances}\\ } where \<^dof> command \value*\ type-checks, expands in an own validation phase -the \instance_of\-term antiquotation, and evaluates the resulting HOL expression +the \Assertion-instances\-term antiquotation, and evaluates the resulting HOL expression above. Assuming an ontology providing the class \Assertion\ having at least the integer attribute \relvce\, the command finally creates an instance of \Assertion\ and binds this to the label \ass\ for further use. @@ -451,6 +451,8 @@ section*[invariants::technical,main_author="Some(@{docitem ''nic''}::author)"] \Term-Context Support, Invariants and Queries in DOF\ (*<*) +(* Ontology example for mathematical papers *) + doc_class myauthor = email :: "string" <= "''''" doc_class mytext_section = @@ -498,12 +500,12 @@ declare[[invariants_checking_with_tactics = false]] text\ To offer a smooth integration into the \<^emph>\formal\ theory development process, - Isabelle/HOL should be able to dynamically interpret the source document. - But the specific antiquotations introduced by Isabelle/DOF are not directly recognized - by Isabelle/HOL, and the process of term checking and evaluation must be enriched. + \<^isabelle> should be able to dynamically interpret the source document. + But the specific antiquotations introduced by \<^dof> are not directly recognized + by \<^isabelle>, and the process of term checking and evaluation must be enriched. Previous works~@{cite "brucker.ea:isabelle-ontologies:2018" and "brucker.ea:isabelledof:2019"} added a validation step for the SML and semi-formal text contexts. - To support Isabelle/DOF antiquotations in the term contexts, the validation step should + To support \<^dof> antiquotations in the term contexts, the validation step should be improved and a new step, which we call \<^emph>\elaboration\ must be added to allow these antiquotations in \\\-terms. The resulting process encompasses the following steps: @@ -511,16 +513,16 @@ text\ \<^item> Infer the type of the term; \<^item> Certify the term; \<^item> Pass on the information to PIDE; - \<^item> Validate the term: the Isabelle/DOF antiquotations terms are parsed and type-checked; - \<^item> Elaborate: the Isabelle/DOF antiquotations terms are expanded. - The antiquotations are replaced by the object in HOL they reference - i.e. a \(\lambda\)-calculus term; + \<^item> Validate the term: the \<^dof> antiquotations terms are parsed and type-checked; + \<^item> Elaborate: the \<^dof> antiquotations terms are expanded. + The antiquotations are replaced by the object in \<^hol> they reference + i.e. a \\\-calculus term; \<^item> Code generation: - \<^item> Evaluation of HOL expressions with ontological annotations, + \<^item> Evaluation of \<^hol> expressions with ontological annotations, \<^item> Generation of ontological invariants processed simultaneously - with the generation of the document (a theory in HOL). + with the generation of the document (a theory in \<^hol>). - Isabelle/HOL provides commands to type-check and print terms (the command \<^theory_text>\term\) + \<^isabelle> provides commands to type-check and print terms (the command \<^theory_text>\term\) and evaluate and print a term (the command \<^theory_text>\value\). We provide the equivalent commands, respectively \<^theory_text>\term*\ and \<^theory_text>\value*\, which support the validation and elaboration phase. @@ -565,7 +567,7 @@ doc_class myconclusion = text_section + \caption{Excerpt of an ontology example for mathematical papers.} \label{fig-ontology-example} \end{figure} - we add up some class instances with the \<^theory_text>\text*\ command, as in \autoref{fig-instances-example}. + we define some class instances with the \<^theory_text>\text*\ command, as in \autoref{fig-instances-example}. \begin{figure} @{boxed_theory_text [display] \ text*[church::myauthor, email="\church@lambda.org\"]\\ @@ -582,8 +584,8 @@ text*[claimNotion::myclaim, authored_by = "{@{myauthor \church\}}", \caption{Some instances of the classes of the ontology in the \autoref{fig-ontology-example}.} \label{fig-instances-example} \end{figure} - In the instance \<^theory_text>\introduction1\, \<^theory_text>\@{author \church\}\ denotes - the instance \<^theory_text>\church\ of the class \<^theory_text>\author\. + In the instance \<^theory_text>\introduction1\, \<^term>\@{myauthor \church\}\ denotes + the instance \<^theory_text>\church\ of the class \<^term>\myauthor\. One can now reference a class instance in a \<^theory_text>\term*\ command. In the command \<^theory_text>\term*\@{myauthor \church\}\\ the term \<^term>\@{myauthor \church\}\ is type-checked, \<^ie>, the command \<^theory_text>\term*\ checks that @@ -610,9 +612,9 @@ declare_reference*["evaluation-example"::side_by_side_figure] text\ The \<^theory_text>\value*\ command \<^theory_text>\value*\email @{author \church\}\\ - type-checks the antiquotation \<^term>\@{author \church\}\, - and then returns the value of the \<^theory_text>\email\ attribute for the \<^theory_text>\church\ instance, - \<^ie> the HOL string \<^term>\''church@lambda.org''\ + type-checks the antiquotation \<^term>\@{myauthor \church\}\, + and then returns the value of the \<^term>\email\ attribute for the \<^theory_text>\church\ instance, + \<^ie> the \<^hol> string \<^term>\''church@lambda.org''\ (see \<^side_by_side_figure>\evaluation-example\). \ @@ -653,7 +655,7 @@ declare_reference*["term-context-equality-evaluation"::figure] text\ We can even compare class instances. \<^figure>\term-context-equality-evaluation\ shows that the two class instances \<^theory_text>\resultProof\ and \<^theory_text>\resultProof2\ are not equivalent - because their attribute \<^theory_text>\property\ differ. + because their attribute \<^term>\property\ differ. \ figure*[ @@ -665,24 +667,25 @@ figure*[ text\ A novel mechanism to specify constraints as invariants is implemented - and can now be specified in common HOL syntax, using the keyword \<^theory_text>\invariant\ + and can now be specified in common \<^hol> syntax, using the keyword \<^theory_text>\invariant\ in the class definition (recall \autoref{fig-ontology-example}). Following the constraints proposed in @{cite "brucker.ea:isabelle-ontologies:2018"}, - one can specify that any instance of a class \<^theory_text>\myresult\ + one can specify that any instance of a class \<^term>\myresult\ finally has a non-empty property list, if its \<^typ>\kind\ is \<^theory_text>\"proof"\ (see the \<^theory_text>\invariant has_property\), or that - the \<^theory_text>\establish\ relation between \<^typ>\myclaim\ and \<^typ>\myresult\ must be defined when an instance - of the class \<^theory_text>\myconclusion\ is defined (see the \<^theory_text>\invariant establish_defined\). + the \<^term>\establish\ relation between \<^typ>\myclaim\ and \<^typ>\myresult\ + must be defined when an instance + of the class \<^term>\myconclusion\ is defined (see the \<^theory_text>\invariant establish_defined\). - In our example, the \<^theory_text>\invariant author_finite\ of the class \<^theory_text>\myintroduction\ enforces - that the user sets the \<^theory_text>\authored_by\ set. - The \<^theory_text>\\\ symbol is reserved and references the future class instance. + In our example, the \<^theory_text>\invariant author_finite\ of the class \<^term>\myintroduction\ enforces + that the user sets the \<^term>\authored_by\ set. + The \\\ symbol is reserved and references the future class instance. By relying on the implementation of the Records - in Isabelle/HOL~@{cite "wenzel:isabelle-isar:2020"}, + in \<^isabelle>~@{cite "wenzel:isabelle-isar:2020"}, one can reference an attribute of an instance using its selector function. - For example, \<^theory_text>\establish \\ denotes the value - of the \<^theory_text>\establish\ attribute - of the future instance of the class \<^theory_text>\myconclusion\. + For example, \<^term>\establish \\ denotes the value + of the \<^term>\establish\ attribute + of the future instance of the class \<^term>\myconclusion\. \ (*<*) @@ -693,16 +696,16 @@ text\ The value of each attribute defined for the instances is checked at run-time against their class invariants. The \<^theory_text>\resultProof\ instance respects the \<^theory_text>\invariant has_property\, - because we specify its attribute \<^theory_text>\evidence\ to the \<^theory_text>\kind\ \<^theory_text>\"proof"\, - we also specify its attribute \<^theory_text>\property\ with a suited value - as a list of \<^theory_text>\"thm"\. + because we specify its attribute \<^term>\evidence\ to the \<^typ>\kind\ \<^theory_text>\"proof"\, + we also specify its attribute \<^term>\property\ with a suited value + as a list of \<^typ>\thm\. In \<^figure>\invariant-checking-figure\, - we try to specify a new instance \<^theory_text>\introduction1\ of the class \<^theory_text>\myintroduction\. + we try to specify a new instance \<^theory_text>\introduction1\ of the class \<^term>\myintroduction\. But an invariant checking error is triggered because we do not respect the constraint specified in the \<^theory_text>\invariant force_level\, - when we specify the \<^theory_text>\level\ attribute of \<^theory_text>\introduction1\ to \<^theory_text>\Some 0\. + when we specify the \<^term>\level\ attribute of \<^theory_text>\introduction1\ to \<^term>\Some 0\. The \<^theory_text>\invariant force_level\ forces the value of the argument - of the attribute \<^theory_text>\level\ to be greater than 1. + of the attribute \<^term>\level\ to be greater than 1. \ figure*[ @@ -718,8 +721,8 @@ declare_reference*["inherited-invariant-checking-figure"::figure] text\ Classes inherit the invariants from their superclass. - As the class \<^theory_text>\myclaim\ is a subsclass - of the class \<^theory_text>\myintroduction\, it inherits the \<^theory_text>\myintroduction\ invariants. + As the class \<^term>\myclaim\ is a subsclass + of the class \<^term>\myintroduction\, it inherits the \<^term>\myintroduction\ invariants. Hence the \<^theory_text>\invariant force_level\ is checked when the instance \<^theory_text>\claimNotion\ is defined, like in \<^figure>\inherited-invariant-checking-figure\. @@ -743,21 +746,22 @@ value*\filter (\\. myresult.evidence \ = argument) @ (*>*) text\ - A new mechanism to make query on instances is available and uses the HOL implementation of lists. + A new mechanism to make query on instances is available and uses + the \<^hol> implementation of lists. Complex queries can then be defined using functions over the instances list. - To get the list of the properties of the instances of the class \<^theory_text>\myresult\, - and the list of the authors of the instances of the class \<^theory_text>\myintroduction\, + To get the list of the properties of the instances of the class \<^term>\myresult\, + and the list of the authors of the instances of the class \<^term>\myintroduction\, one can use the command \<^theory_text>\value*\: @{theory_text [display,indent=10, margin=70] \ value*\map (myresult.property) @{myresult-instances}\ value*\map (mytext_section.authored_by) @{myintroduction-instances}\ \} - To get the list of the instances of the class \<^theory_text>\myresult\ whose \<^theory_text>\evidence\ is a \<^theory_text>\"proof"\, - on can use the command: + To get the list of the instances of the class \<^term>\myresult\ + whose \<^term>\evidence\ is a \<^theory_text>\"proof"\, on can use the command: @{theory_text [display,indent=10, margin=70] \ value*\filter (\\. myresult.evidence \ = proof) @{myresult-instances}\ \} - To get the list of the instances of the class \<^theory_text>\myintroduction\ whose \<^theory_text>\level\ > 1, + To get the list of the instances of the class \<^term>\myintroduction\ whose \<^term>\level\ > 1, on can use the command: @{theory_text [display,indent=10, margin=70] \ value*\filter (\\. the (mytext_section.level \) > 1) @{myintroduction-instances}\ @@ -770,8 +774,176 @@ section*[ontoexample::text_section,main_author="Some(@{docitem ''idir''}::author subsection\Engineering Example : An Extract from PLib\ -subsection\Mathematics Example : An Extract from OntoMathPro\ +subsection\Mathematics Example : An Extract from OntoMath\textsuperscript{PRO}\ +(*<*) +(* OntoMathPro_Ontology example *) + +datatype dc = creator string | title string + +datatype owl = + backwardCompatibleWith string + | deprecated string + | incompatibleWith string + | priorVersion string + | versionInfo string + +datatype rdfs = + comment string + | isDefinedBy string + | label string + | seeAlso string + +datatype annotation = DC dc | OWL owl | RDFS rdfs + +onto_class Top = + Annotations :: "annotation list" + +onto_class Field_of_mathematics = + Annotations :: "annotation list" + invariant restrict_annotation_F ::"set (Annotations \) \ + range (RDFS o label) \ range (RDFS o comment)" + +onto_class Mathematical_knowledge_object = + Annotations :: "annotation list" + invariant restrict_annotation_M ::"set (Annotations \) \ + range (RDFS o label) \ range (RDFS o comment)" + +onto_class assoc_F_M = + contains:: "(Field_of_mathematics \ Mathematical_knowledge_object) set" + invariant contains_defined :: "\ x. x \ Domain (contains \) + \ (\ y \ Range (contains \). (x, y) \ contains \)" + +onto_class assoc_M_F = + belongs_to :: "(Mathematical_knowledge_object \ Field_of_mathematics) set" + invariant belong_to_defined :: "\ x. x \ Domain (belongs_to \) + \ (\ y \ Range (belongs_to \). (x, y) \ belongs_to \)" + +onto_class assoc_M_M = + is_defined_by :: "(Mathematical_knowledge_object \ Mathematical_knowledge_object) set" + invariant is_defined_by_defined :: "\ x. x \ Domain (is_defined_by \) + \ (\ y \ Range (is_defined_by \). (x, y) \ is_defined_by \)" +(*typedef 'a A'_scheme = + "{x :: 'a A_scheme. " +*) + +onto_class assoc_M_M' = + "defines" :: "(Mathematical_knowledge_object \ Mathematical_knowledge_object) set" + invariant defines_defined :: "\ x. x \ Domain (defines \) + \ (\ y \ Range (defines \). (x, y) \ defines \)" + +onto_class assoc_M_M_see_also = + see_also :: "(Mathematical_knowledge_object rel) set" + invariant see_also_trans :: "\ r \ (see_also \). trans r" + invariant see_also_sym :: "\ r \ (see_also \). sym r" + +onto_class Problem = Mathematical_knowledge_object + + Annotations :: "annotation list" + +onto_class Method = Mathematical_knowledge_object + + Annotations :: "annotation list" + +onto_class assoc_Problem_Method = + is_solved_by :: "(Problem \ Method) set" + invariant is_solved_by_defined :: "\ x. x \ Domain (is_solved_by \) + \ (\ y \ Range (is_solved_by \). (x, y) \ is_solved_by \)" + +onto_class assoc_Method_Problem = + solves :: "(Method \ Problem) set" + invariant solves_defined :: "\ x. x \ Domain (solves \) + \ (\ y \ Range (solves \). (x, y) \ solves \)" + +(*>*) + +text\ + The \<^emph>\OntoMath\textsuperscript{PRO}\ ontology @{cite "DBLP:journals/corr/NevzorovaZKL14"} + is an OWL ontology of mathematical knowledge concepts. + It posits the ISA semantics @{cite "1654194"} for hierarchies of mathematical knowledge objects, + and defines these objects as two hierarchies of classes: + a taxonomy of the fields of mathematics and a taxonomy of mathematical knowledge objects. + It defines two main type of relations for these two taxonomies: + directed relations between elements of the two hierarchies + like \<^term>\belongs_to\, \<^term>\contains\, \<^term>\defines\, \<^term>\is_defined_by\, \<^term>\solves\, + \<^term>\is_solved_by\, and a symmetric transitive associative relation \<^term>\see_also\ + between two mathematical knowledge objects. + It also represents links with external resources such as DBpedia + with annotations properties @{cite "Parsia:12:OWO"}. + \<^dof> covers a wide range of the OWL concepts used by the \<^emph>\OntoMath\textsuperscript{PRO}\ ontology. + We can represent the annotations properties as datatypes and + then attach them as an attributes list to a class. + For example the declaration: +@{theory_text [display,indent=10, margin=70] \ +datatype dc = creator string | title string +datatype owl = backwardCompatibleWith string + | deprecated string + | incompatibleWith string + | priorVersion string + | versionInfo string +datatype rdfs = comment string + | isDefinedBy string + | label string + | seeAlso string +datatype annotation = DC dc | OWL owl | RDFS rdfs + +onto_class Field_of_mathematics = + Annotations :: "annotation list" + invariant restrict_annotation_F ::"set (Annotations \) \ + range (RDFS o label) \ range (RDFS o comment)" + +\} + defines the class \<^term>\Field_of_mathematics\ with an attribute \<^term>\Annotations\ + which is a list of \<^typ>\annotation\s. + We can even constraint the type of allowed \<^typ>\annotation\s with an invariant. + Here the \<^theory_text>\invariant restrict_annotation_F\ forces the \<^typ>\annotation\s to be + a \<^term>\label\ or a \<^term>\comment\. + Subsumption relation is straightforward. + The ontology \<^emph>\OntoMath\textsuperscript{PRO}\ defines + a \<^term>\Problem\ and a \<^term>\Method\ + as subclasses of the class \<^term>\Mathematical_knowledge_object\. + It gives in \<^dof>: +@{theory_text [display,indent=10, margin=70] \ +onto_class Problem = Mathematical_knowledge_object + + Annotations :: "annotation list" + +onto_class Method = Mathematical_knowledge_object + + Annotations :: "annotation list" +\} + We can express the relations between the two taxonomies + with association \<^theory_text>\onto_class\es which specify + the relation as an attribute and enforces the relation with an \<^theory_text>\invariant\. + The two directed relations \<^term>\is_solved_by\ and \<^term>\solves\ + between \<^term>\Problem\ and a \<^term>\Method\ can be represented in \<^dof> like this: +@{theory_text [display,indent=10, margin=70] \ + +onto_class assoc_M_M_see_also = + see_also :: "(Mathematical_knowledge_object rel) set" + invariant see_also_trans :: "\ r \ (see_also \). trans r" + invariant see_also_sym :: "\ r \ (see_also \). sym r" + +onto_class Method = Mathematical_knowledge_object + + Annotations :: "annotation list" + +onto_class assoc_Problem_Method = + is_solved_by :: "(Problem \ Method) set" + invariant is_solved_by_defined :: "\ x. x \ Domain (is_solved_by \) + \ (\ y \ Range (is_solved_by \). (x, y) \ is_solved_by \)" + +onto_class assoc_Method_Problem = + solves :: "(Method \ Problem) set" + invariant solves_defined :: "\ x. x \ Domain (solves \) + \ (\ y \ Range (solves \). (x, y) \ solves \)" +\} + where the attributes \<^term>\is_solved_by\ and \<^term>\solves\ define the relations + of the classes and the invariants \<^theory_text>\is_solved_by_defined\ and \<^theory_text>\solves_defined\ enforce + the existence of the relations when one define instances of the classes. + + \<^dof> as a framework allows to define an ontology and specify constraints + on its concepts, and dynamically checks at run-time the concepts and instances. + It offers an environment to define and test ontologies in an integrated document, + where all the knowledge and the proof-checking can be specified, + and thus can be a solution to go over + the trade-off between plain vocabularies and highly formalized models. +\ section*[concl::conclusion]\Conclusion\ subsection*[rw::related_work]\Related Works\