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#>`