RDF triples largely follow (an extension of) the [Upper Library Ontology](https://kwarc.info/kohlhase/papers/cicm19-ulo.pdf). #### Some Abbreviations | abbreviation | URI | |-----|---------------------------------------------| |`rdf`|`http://www.w3.org/1999/02/22-rdf-syntax-ns`| |`ulo`|`http://mathhub.info/ulo`| | `myarch` | `http://mathhub.info/My/Archive` | ### Generic Stuff Assume we have an sTeX archive `My/Archive` with narrative URI `http://mathhub.info/My/Archive`. Then MMT generates the following triples: - `<mmt://memory/archive#My> <rdf:#type> <ulo:#library_group>` - `<mmt://memory/archive#My/Archive> <rdf:#type> <ulo:#library>` - `<mmt://memory/archive#My> <ulo:#contains> <mmt://memory/archive#My/Archive>` Assume we have an stex-file `foo.en.tex` in the directory `source/mod/example` in `My/Archive`. When being built by MMT, this generates the following triples: ***Note:** MMT-URIs always have a `#` appended at the end; this is necessary to make them valid RDF-IRIs.* ***Note also:** We use the narrative URI of the archive for everything; including files. This makes their IRIs independent of a user's local file system.* - `<myarch:/source/mod/example/foo.en.tex#> <rdf:#type> <ulo:#file>` (Note, that the file name explicitly carries the `source` path component, so we can distinguish between e.g. generated files and source files) - `<myarch:/mod/example/foo.en.omdoc#> <rdf:#type> <ulo:#document>` (the MMT-document generated from the file) - `<myarch:/mod/example/foo.en.omdoc?en#> <rdf:#type> <ulo:#theory>` (the "language module"; an MMT-theory containing all learning objects, among other things) - `<myarch:/mod/example/foo.en.omdoc?en#> <rdf:#type> <ulo:#language-module>` - `<myarch:/mod/example/foo.en.omdoc?en#> <ulo:#has-language> "en"` - `<myarch:/mod/example/foo.omdoc#> <ulo:#has-language-module> <myarch:/mod/example/foo.en.omdoc?en#>` (a dummy element that only exists to have multiple language modules in different languages associated with it - it only exists as a subject in the triple store; MMT can't actually resolve the URI to anything specific) - `<mmt://memory/archive#My/Archive> <ulo:#contains> <myarch:/foo.en.tex#>` - `<myarch:/source/mod/example/foo.en.tex#> <ulo:#contains> <myarch:/mod/example/foo.en.omdoc#>` - `<myarch:/mod/example/foo.en.omdoc#> <ulo:#specifies> <myarch:/mod/example/foo.en.omdoc?en#>` - `<myarch:/source/mod/example/foo.en.tex#> <ulo:#last-checked-at> (timestamp:Long)` **In the following, let `myarch::=http://mathhub.info/My/Archive/mod/example`** ### Declarations - A `\usemodule{bar}` is translated to an include in the corresponding language module; hence yields the triple `<myarch:/foo.en.omdoc?en#> <ulo:#includes> <...?bar#>` - A section `\begin{sfragment}` generates a document with name `id` or (if no `id` is given) autogenerated name: - `<myarch:/foo.en.omdoc/id#> <rdf:#type> <ulo:#document>` - `<myarch:/foo.en.omdoc#> <ulo:#specifies> <myarch:/foo.en.omdoc/id#>` **TODO** should probably be treated similar to learning objects. There's some code to be cleaned up here. - A variable declaration (i.e. `\vardef{vA}` or `\varseq{vA}`) generates a constant in the corresponding language module, hence: - `<myarch:/foo.en.omdoc?en?vA#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en?vA#> <rdf:#type> <ulo:#variable>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?vA#>` - A *module* `\begin{smodule}{Foo}` is translated to an *MMT theory*, which is immediately included in the language module: - `<myarch:?Foo#> <rdf:#type> <ulo:#theory>` - `<myarch:/foo.en.omdoc?en#> <ulo:#includes> <myarch:?Foo#>` - An `\importmodule{bar}` is translated to an include of the parent module, i.e. `<myarch:?Foo#> <ulo:#includes> <...?bar#>` - A symbol declaration `\symdecl{A}` generates a *constant* in the containing theory; i.e.: - `<myarch:?Foo?A#> <rdf:#type> <ulo:#constant>` - `<myarch:?Foo#> <ulo:#specifies> <myarch:?Foo?A#>` - `\begin{mathstructure}` generates a theory *and* a constant ***TODO:** Check what actually happens* - An `\inputref{some/file.tex}` generates `<myarch:/foo.en.omdoc#> <ulo:#contains> <.../some/file.omdoc#>` (i.e. it relates the corresponding MMT documents) ### Learning Objects There are five types of learning objects: 1. Symbol documentations `\begin{sparagraph}[style=symdoc]` 2. Definitions `\begin{sdefinition}` 3. Examples `\begin{sexample}` 4. Assertions `\begin{sassertion}` 5. Problems `\begin{sproblem}` All of them generate a *constant* with auto-generated name `loname` in the language module, with the HTML as `OMFOREIGN`-definiens. Symbol documentations, definitions and examples carry a list `fors` of symbol URIs which are either explicitly given (via `[for={...,...}]`) or (in the case of 1. and 2.) determined via occurrences of `\definiendum/\definame`. 1. A symbol documentation `loname` generates: - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#para>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?loname#>` - for every symbol `S` in the `fors`-list: `<...?S#> <ulo:#docref> <myarch:/foo.en.omdoc?en?loname#>` 2. A definition `loname` generates: - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#definition>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?loname#>` - for every symbol `S` in the `fors`-list: `<myarch:/foo.en.omdoc?en?loname#> <ulo:#defines> <...?S#>` and `<...?S#> <ulo:#docref> <myarch:/foo.en.omdoc?en?loname#>` 3. An example `loname` generates: - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#example>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?loname#>` - for every symbol `S` in the `fors`-list: `<myarch:/foo.en.omdoc?en?loname#> <ulo:#example-for> <...?S#>` 4. An assertion `loname` generates: - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#statement>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?loname#>` - If the statement has a *name* `S` or a `for=S`: `<...?S#> <ulo:#docref> <myarch:/foo.en.omdoc?en?loname#>` 4. An problem `loname` generates both a theory (for including/local symbol declarations) and a constant in the language module: - `<myarch:?loname> <rdf:#type> <ulo:#theory>` - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en?loname#> <rdf:#type> <ulo:#problem>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?loname#>` - `<myarch:/foo.en.omdoc#> <ulo:#specifies> <myarch:?loname#>` - An annotation `\precondition{dimension}{S}` additionally generates a blank node `B` with: - `<myarch:/foo.en.omdoc?en?loname#> <ulo:#precondition> B` - `B <ulo:#cognitive-dimension> "dimension"` - `B <ulo:#specifies> <...?S#>` - An annotation `\objective{dimension}{S}` additionally generates a blank node `B` with: - `<myarch:/foo.en.omdoc?en?loname#> <ulo:#objective> B` - `B <ulo:#cognitive-dimension> "dimension"` - `B <ulo:#specifies> <...?S#>` ### Terms/Symbol References **Definition** let the *parent* `P` of an (HTML DOM) element be either 1. the constant corresponding to the nearest ancestor that is a learning object, or 2. the language module, if none exists. - A *symbolic expression*/*term* occurring anywhere in a source file (e.g. `\plus{\vA,\vB}`) generates a *constant* in the corresponding language module **iff** it is not just a constant/variable reference: - `<myarch:/foo.en.omdoc?en?term1#> <rdf:#type> <ulo:#constant>` - `<myarch:/foo.en.omdoc?en#> <ulo:#specifies> <myarch:/foo.en.omdoc?en?term1#>` - Symbols `S`occuring in the term are associated via `<myarch:/foo.en.omdoc?en?term1#> <ulo:#crossrefs> <...?S#>` (...I think. The default MMT relational extractor takes care of that - it might be, that it additional differentiates between type and definiens components) - `\symref/\symname` et al are treated exactly like constant/variable references. i.e. `$\plus!$` and `\symname{plus}` are both considered `OMS`s and do not generate a constant. Instead, for such a reference to a symbol `S`, we do - `<...?P#> <ulo:#crossrefs> <...?S#>`