| 2 | | Welcome to the [wiki:JOBAD] demo for the [http://sites.google.com/a/fh-hannover.de/aimashup/ AI Mashup Challenge at ESWC 2010]! This page supplements our [http://sites.google.com/a/fh-hannover.de/aimashup/home/jobad subpage of the AI Mashup homepage]. |
| 3 | | |
| 4 | | = JOBAD = |
| 5 | | |
| 6 | | JOBAD is a versatile architecture that makes mathematical documents interactive. It improves comprehension by providing the reader with additional information on demand, and it allows the reader to customize a document's appearance to his preferences. |
| 7 | | |
| 8 | | == Background == |
| 9 | | |
| 10 | | Mathematics is hard. Mathematical documents are concise and minimalistic. They talk about objects that are so abstract that non-experts have difficulties remembering their construction and predicting their properties. They pile layers and layers of definitions and proved assertions. As a consequence, a document usually depends on others, which in turn depends on further documents. In a nutshell, mathematics is hard because it is embodied in documents that are optimized for the initiated, at the cost of being virtually unintelligible to the casual reader. Unfortunately, with 120,000 articles being published per year in mathematical journals, everyone is a casual reader (almost any time). |
| 11 | | |
| 12 | | == Solution == |
| 13 | | |
| 14 | | JOBAD is an architecture for providing mashup services in mathematical documents, alleviating some of the comprehension barriers by providing the necessary information ''in time'' and ''in place''. JOBAD is a JavaScript library that makes specially annotated XHTML+MathML+RDFa documents interactive and connects them to mathematical services on the web. |
| 15 | | |
| 16 | | [[Image(architecture2010.png,right,403px)]] |
| 17 | | |
| 18 | | == Services == |
| 19 | | |
| 20 | | ''(go on, describing what we have at the moment)'' |
| 21 | | |
| 22 | | * The MMT web server ([MMT:WikiStart MMT backend]) is implemented on top of the MMT language, an advanced module system for formalized mathematics that can integrate mathematical content from different foundations and is designed to perform well on a web scale. The MMT web server permits to interact with MMT knowledge representations. |
| 23 | | |
| 24 | | Typically mathematical content is stored decentrally in many interlinked knowledge bases. For example, our main storage is a dedicated XML database, but MMT also has to work with other repositories or even local files. Moreover, it is typical that a mathematical theory, e.g., for the ring of complex matrices, depends on theories stored elsewhere, e.g., ring theory and complex numbers (and eventually set theory). Therefore, the web server must be decoupled from the content storage, and it is typical that it has to interact with different backends to serve a single request. |
| 25 | | |
| 26 | | To render machine-oriented knowledge representations in human-readable form makes notations indispensable. However, in mathematics, notations are often not stored together with the content. For example, a user may store her own notationIn fact, typically different users have their own notations. Therefore, the MMT browser has to pull notations from even different backends. |
| 27 | | |
| 28 | | Currently the MMT web server is provided as a standalone war file that can be deployed on any server, even as a local proxy, with a configurable list of backends. A backend is selected based on the canonical URI of an MMT knowledge item using an XML catalogue. Possible backends are plain web servers, local directories, and the TNTbase XML database. For the latter, we have developed a set of XQuery functions that implement MMT functionality. |
| 29 | | |
| 30 | | Most importantly, these functions can compute the forward and backward dependency closure of MMT knowledge items using indexes for the ABoxes of the MMT ontology. For example, when rendering a theory T, the MMT web server can retrieve all notations occurring in any theory transitively imported into T from TNTbase in constant time. This yields a significant speed-up over the otherwise necessary iterated retrievals of imported theories and thus makes a large scale interactive web service for mathematics feasible. |
| 31 | | |
| 32 | | * Computer Science lecture notes: ''(describe)'' |
| 33 | | * other? ''(old unit conversion, computer algebra?)'' |
| 34 | | |
| 35 | | ''(news compared to 2009 at a glance, say that it is currently undergoing a major overhaul)'' |
| 36 | | |
| 37 | | == Integrated Demo Applications == |
| 38 | | |
| 39 | | ''(point to concrete demos)'' |
| 40 | | |
| 41 | | * Logic Atlas: The LATIN logic atlas is a recently started DFG-funded project in which we use MMT as the representation of a web-scalable encyclopedia of formal logic. The MMT web server will be the central component, and we use JOBAD as the client-side software to interact with the atlas. A demo installation is available at http://cds.omdoc.org:8181/logics/first-order/proof_theory/derived.omdoc???present_foundations/lf/mathml.omdoc?mathml. |
| 42 | | It retrieves the content (here with MMT URI http://cds.omdoc.org/logics/first-order/proof_theory/derived.omdoc) and the notations (here the notation style with MMT URI http://cds.omdoc.org/foundations/lf/mathml.omdoc?mathml) from the respective backend (including all relevant imported knowledge items) and uses the notations to transform the content into JOBAD-enabled XHMTL+presentation MathML. This supports in particular: |
| 43 | | * Folding of mathematical expressions: Via the context menu, users can fold parts of a mathematical expressions based on its semantic structure, i.e., folding on a symbol hides the smallest surrounding subexpression. |
| 44 | | * Cross-referencing: By left-clicking on symbols, users can navigate the LATIN graph. Here JOBAD has to compute the needed target URL based on the desired notations. |
| 45 | | * Type and definitins lookup: Via the context of symbols, it is possible to obtain the type or the definition of a mathematical symbol. Here the MMT-JOBAD mashup not only has to retrieve the respective type/definition but also render using the notations corresponding to the currently viewed document. |
| 46 | | * Interactive visibility: The MMT server marks up the visibility of optional expressions such as redundant brackets, implicit arguments, or variable types using logical formulas whose value depends on some user-defined variables. JOBAD spots those variables and produces GUI items for them such as checkboxes or sliders. Depending on their values, JOBAD computes the visibility of document parts and including mathematical subexpressions. |
| 47 | | |
| 48 | | * Computer science lecture notes: ''(definition lookup in TNTBase: same as 2009 but with new JavaScript service API and working context menu)'' |
| 49 | | * ''maybe others'' |
| | 2 | Welcome to the [wiki:JOBAD] demo for the [http://sites.google.com/a/fh-hannover.de/aimashup/ AI Mashup Challenge at ESWC 2010]! All up-to-date information can be found on [http://sites.google.com/a/fh-hannover.de/aimashup/home/jobad our subpage of the AI Mashup homepage]. |
