40 Result(s)
within
Chapter
Michael Kohlhase
Mathematical Logic and Formal Languages
Theory of Computation
-
Chapter and Conference Paper
A Proof Theoretic Interpretation of Model Theoretic Hiding
Logical frameworks like LF are used for formal representations of logics in order to make them amenable to formal machine-assisted meta-reasoning. While the focus has originally been on logics with a proof the...
-
Chapter and Conference Paper
Towards Logical Frameworks in the Heterogeneous Tool Set Hets
LF is a meta-logical framework that has become a standard tool for representing logics and studying their properties. Its focus is proof theoretic, employing the Curry-Howard isomorphism: propositions are repr...
-
Chapter
Appendix
In this appendix, we document the changes of the OMDoc format over the versions, provide quick reference tables, and discuss the validation helps.
-
Chapter
The OMDoc Document Format
The OMDoc ( Open Mathematical Documents) format is a content markup scheme for (collections of) mathematical documents including articles, textbooks, interactive books, and courses. OMDoc also serves as the con...
-
Chapter
OMDoc Applications, Tools, and Projects
In this part we will address current applications, tools and projects using the OMDoc format. We will first discuss the possibilities and tools of processing documents in the OMDoc format via style sheets with th...
-
Chapter
Quick-Reference Table to the OMDoc Attributes
-
Chapter
The RelaxNG Schemata for Mathematical Objects
For completeness we reprint the RelaxNG schemata for the external formats OMDoc makes use of.
-
Chapter
Communication with and Between Mathematical Software Systems
OMDoc can be used as content language for communication protocols between mathematical software systems on the Internet. The ability to specify the context and meaning of the mathematical...
-
Chapter
OMDoc as a Modular Format
A modular approach to design is generally accepted as best practice in the development of any type of complex application. It separates the application’s functionality into a number of “building blocks” or “mo...
-
Chapter
Metadata (Modules DC and CC)
Metadata is “data about data” — in the case of OMDoc data about documents, such as titles, authorship, language usage, or administrative aspects like modification dates, distribution rights, and identifiers. To a...
-
Chapter
Mathematical Text (Modules MTXT and RT)
The everyday mathematical language used in textbooks, conversations, and written onto blackboards all over the world consists of a rigorous, slightly stylized version of natural language interspersed with math...
-
Chapter
Complex Theories (Modules CTH and DG)
In Section 15.6 we have presented a notion of theory and inheritance that is sufficient for simple applications like content dictionaries that informally (though presumably rigorously) define the static meanin...
-
Chapter
Setting the Stage for Open Mathematical Documents
In this part of the book we will look at the problem of marking up mathematical knowledge and mathematical documents in general, situate the OMDoc format, and compare it to other formats like OpenMath and MathML.
-
Chapter
Abstract Data Types (Module ADT)
Most specification languages for mathematical theories support definition mechanisms for sets that are inductively generated by a set of constructors and recursive functions on these under the heading of abstract...
-
Chapter
Auxiliary Elements (Module EXT)
Up to now, we have been mainly concerned with providing elements for marking up the inherent structure of mathematical knowledge in mathematical statements and theories. Now, we interface OMDoc documents with the...
-
Chapter
Markup for Mathematical Knowledge
Mathematicians make use of various kinds of documents (e.g. e-mails, letters, pre-prints, journal articles, and textbooks) for communicating mathematical knowledge. Such documents employ specialized notational...
-
Chapter
Document Models for OMDoc
In almost all XML applications, there is a tension between the document view and the object view of data; after all, XML is a document-oriented interoperability framework for exchanging data objects. The quest...
-
Chapter
An OMDoc Primer
This part of the book provides an easily approachable description of the OMDoc format by way of paradigmatic examples of OMDoc documents. The primer should be used alongside the formal descriptions of the languag...
-
Chapter
OMDoc Resources
In this chapter we will describe various public resources for working with the OMDoc format.
-
Chapter
OpenMath Content Dictionaries
Content Dictionaries are structured documents used by the OpenMath standard [BCC + 04] to codify knowledge about mathematical symbols and concepts used in the representation of mathematical formulae. They differ ...
