Showing 1–31 of 31 results for author: Kohlhase, M

Context Graphs for Legal Reasoning and Argumentation

Authors: Max Rapp, Axel Adrian, Michael Kohlhase

Abstract: We propose a new, structured, logic-based framework for legal reasoning and argumentation: Instead of using a single, unstructured meaning space, theory graphs organize knowledge and inference into collections of modular meaning spaces organized by inheritance and interpretation. Context graphs extend theory graphs by attack relations and interpret theories as knowledge contexts of agents in argum… ▽ More We propose a new, structured, logic-based framework for legal reasoning and argumentation: Instead of using a single, unstructured meaning space, theory graphs organize knowledge and inference into collections of modular meaning spaces organized by inheritance and interpretation. Context graphs extend theory graphs by attack relations and interpret theories as knowledge contexts of agents in argumentation. We introduce the context graph paradigm by modeling the well-studied case Popov v. Hayashi, concentrating on the role of analogical reasoning in context graphs. △ Less

Submitted 1 July, 2020; originally announced July 2020.

Making Isabelle Content Accessible in Knowledge Representation Formats

Authors: Michael Kohlhase, Florian Rabe, Makarius Wenzel

Abstract: The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved… ▽ More The libraries of proof assistants like Isabelle, Coq, HOL are notoriously difficult to interpret by external tools: de facto, only the prover itself can parse and process them adequately. In the case of Isabelle, an export of the library into a FAIR (Findable, Accessible, Interoperable, and Reusable) knowledge exchange format was already envisioned by the authors in 1999 but had previously proved too difficult. After substantial improvements of the Isabelle Prover IDE (PIDE) and the OMDoc/Mmt format since then, we are now able to deliver such an export. Concretely we present an integration of PIDE and MMT that allows exporting all Isabelle libraries in OMDoc format. Our export covers the full Isabelle distribution and the Archive of Formal Proofs (AFP) -- more than 12 thousand theories and locales resulting in over 65GB of OMDoc/XML. Such a systematic export of Isabelle content to a well-defined interchange format like OMDoc enables many applications such as dependency management, independent proof checking, or library search. △ Less

Submitted 5 May, 2020; originally announced May 2020.

MSC Class: 68V20 68V30

Experiences from Exporting Major Proof Assistant Libraries

Authors: Michael Kohlhase, Florian Rabe

Abstract: The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented tremendous theo… ▽ More The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented tremendous theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution and our experiences will prove valuable to others undertaking such efforts. △ Less

Submitted 5 May, 2020; originally announced May 2020.

MSC Class: 68V30 68V20

The Space of Mathematical Software Systems -- A Survey of Paradigmatic Systems

Authors: Katja Bercic, Jacques Carette, William M. Farmer, Michael Kohlhase, Dennis Müller, Florian Rabe, Yasmine Sharoda

Abstract: Mathematical software systems are becoming more and more important in pure and applied mathematics in order to deal with the complexity and scalability issues inherent in mathematics. In the last decades we have seen a cambric explosion of increasingly powerful but also diverging systems. To give researchers a guide to this space of systems, we devise a novel conceptualization of mathematical soft… ▽ More Mathematical software systems are becoming more and more important in pure and applied mathematics in order to deal with the complexity and scalability issues inherent in mathematics. In the last decades we have seen a cambric explosion of increasingly powerful but also diverging systems. To give researchers a guide to this space of systems, we devise a novel conceptualization of mathematical software that focuses on five aspects: inference covers formal logic and reasoning about mathematical statements via proofs and models, typically with strong emphasis on correctness; computation covers algorithms and software libraries for representing and manipulating mathematical objects, typically with strong emphasis on efficiency; concretization covers generating and maintaining collections of mathematical objects conforming to a certain pattern, typically with strong emphasis on complete enumeration; narration covers describing mathematical contexts and relations, typically with strong emphasis on human readability; finally, organization covers representing mathematical contexts and objects in machine-actionable formal languages, typically with strong emphasis on expressivity and system interoperability. Despite broad agreement that an ideal system would seamlessly integrate all these aspects, research has diversified into families of highly specialized systems focusing on a single aspect and possibly partially integrating others, each with their own communities, challenges, and successes. In this survey, we focus on the commonalities and differences of these systems from the perspective of a future multi-aspect system. △ Less

Submitted 12 February, 2020; originally announced February 2020.

GF + MMT = GLF -- From Language to Semantics through LF

Authors: Michael Kohlhase, Jan Frederik Schaefer

Abstract: These days, vast amounts of knowledge are available online, most of it in written form. Search engines help us access this knowledge, but aggregating, relating and reasoning with it is still a predominantly human effort. One of the key challenges for automated reasoning based on natural-language texts is the need to extract meaning (semantics) from texts. Natural language understanding (NLU) sy… ▽ More These days, vast amounts of knowledge are available online, most of it in written form. Search engines help us access this knowledge, but aggregating, relating and reasoning with it is still a predominantly human effort. One of the key challenges for automated reasoning based on natural-language texts is the need to extract meaning (semantics) from texts. Natural language understanding (NLU) systems describe the conversion from a set of natural language utterances to terms in a particular logic. Tools for the co-development of grammar and target logic are currently largely missing. We will describe the Grammatical Logical Framework (GLF), a combination of two existing frameworks, in which large parts of a symbolic, rule-based NLU system can be developed and implemented: the Grammatical Framework (GF) and MMT. GF is a tool for syntactic analysis, generation, and translation with complex natural language grammars and MMT can be used to specify logical systems and to represent knowledge in them. Combining these tools is possible, because they are based on compatible logical frameworks: Martin-Löf type theory and LF. The flexibility of logical frameworks is needed, as NLU research has not settled on a particular target logic for meaning representation. Instead, new logics are developed all the time to handle various language phenomena. GLF allows users to develop the logic and the language parsing components in parallel, and to connect them for experimentation with the entire pipeline. △ Less

Submitted 23 October, 2019; originally announced October 2019.

Comments: In Proceedings LFMTP 2019, arXiv:1910.08712

Journal ref: EPTCS 307, 2019, pp. 24-39

TGView3D System Description: 3-Dimensional Visualization of Theory Graphs

Authors: Richard Marcus, Michael Kohlhase, Florian Rabe

Abstract: We describe TGView3D, an interactive 3D graph viewer optimized for exploring theory graphs. To exploit the three spatial dimensions, it extends a force-directed layout with a hierarchical component. Because of the limitations of regular displays, the system also supports the use of a head-mounted display and utilizes several virtual realty interaction concepts. We describe TGView3D, an interactive 3D graph viewer optimized for exploring theory graphs. To exploit the three spatial dimensions, it extends a force-directed layout with a hierarchical component. Because of the limitations of regular displays, the system also supports the use of a head-mounted display and utilizes several virtual realty interaction concepts. △ Less

Submitted 27 February, 2020; v1 submitted 16 May, 2019; originally announced May 2019.

Comments: 5 pages, 2 figures, fixed typo

The Theorem Prover Museum -- Conserving the System Heritage of Automated Reasoning

Authors: Michael Kohlhase

Abstract: We present the Theorem Prover Museum, and initiative to conserve -- and make publicly available -- the sources and source-related artefacts of automated reasoning systems. Theorem provers have been at the forefront of Artificial Intelligence, stretching the limits of computation, and incubating many innovations we take for granted today. Without the systems themselves as preserved cultural artefac… ▽ More We present the Theorem Prover Museum, and initiative to conserve -- and make publicly available -- the sources and source-related artefacts of automated reasoning systems. Theorem provers have been at the forefront of Artificial Intelligence, stretching the limits of computation, and incubating many innovations we take for granted today. Without the systems themselves as preserved cultural artefacts, future historians will have difficulties to study the history of science and engineering in our discipline. △ Less

Submitted 23 April, 2019; originally announced April 2019.

Big Math and the One-Brain Barrier A Position Paper and Architecture Proposal

Authors: Jacques Carette, William M. Farmer, Michael Kohlhase, Florian Rabe

Abstract: Over the last decades, a class of important mathematical results have required an ever increasing amount of human effort to carry out. For some, the help of computers is now indispensable. We analyze the implications of this trend towards "big mathematics", its relation to human cognition, and how machine support for big math can be organized. The central contribution of this position paper is an… ▽ More Over the last decades, a class of important mathematical results have required an ever increasing amount of human effort to carry out. For some, the help of computers is now indispensable. We analyze the implications of this trend towards "big mathematics", its relation to human cognition, and how machine support for big math can be organized. The central contribution of this position paper is an information model for "doing mathematics", which posits that humans very efficiently integrate four aspects: inference, computation, tabulation, and narration around a well-organized core of mathematical knowledge. The challenge for mathematical software systems is that these four aspects need to be integrated as well. We briefly survey the state of the art. △ Less

Submitted 22 October, 2019; v1 submitted 23 April, 2019; originally announced April 2019.

Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach

Authors: Paul-Olivier Dehaye, Michael Kohlhase, Alexander Konovalov, Samuel Lelièvre, Markus Pfeiffer, Nicolas M. Thiéry

Abstract: OpenDreamKit --- "Open Digital Research Environment Toolkit for the Advancement of Mathematics" --- is an H2020 EU Research Infrastructure project that aims at supporting, over the period 2015--2019, the ecosystem of open-source mathematical software systems. From that, OpenDreamKit will deliver a flexible toolkit enabling research groups to set up Virtual Research Environments, customised to meet… ▽ More OpenDreamKit --- "Open Digital Research Environment Toolkit for the Advancement of Mathematics" --- is an H2020 EU Research Infrastructure project that aims at supporting, over the period 2015--2019, the ecosystem of open-source mathematical software systems. From that, OpenDreamKit will deliver a flexible toolkit enabling research groups to set up Virtual Research Environments, customised to meet the varied needs of research projects in pure mathematics and applications. An important step in the OpenDreamKit endeavor is to foster the interoperability between a variety of systems, ranging from computer algebra systems over mathematical databases to front-ends. This is the mission of the integration work package (WP6). We report on experiments and future plans with the \emph{Math-in-the-Middle} approach. This information architecture consists in a central mathematical ontology that documents the domain and fixes a joint vocabulary, combined with specifications of the functionalities of the various systems. Interaction between systems can then be enriched by pivoting off this information architecture. △ Less

Submitted 21 March, 2016; originally announced March 2016.

Comments: 15 pages, 7 figures

Realms: A Structure for Consolidating Knowledge about Mathematical Theories

Authors: Jacques Carette, William M. Farmer, Michael Kohlhase

Abstract: Since there are different ways of axiomatizing and develo** a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We introduce the notion of a realm as a structure for consolidating knowledge about a mathematical theory. A realm contains several axiomatizations of a theory that are separately developed. View… ▽ More Since there are different ways of axiomatizing and develo** a mathematical theory, knowledge about a such a theory may reside in many places and in many forms within a library of formalized mathematics. We introduce the notion of a realm as a structure for consolidating knowledge about a mathematical theory. A realm contains several axiomatizations of a theory that are separately developed. Views interconnect these developments and establish that the axiomatizations are equivalent in the sense of being mutually interpretable. A realm also contains an external interface that is convenient for users of the library who want to apply the concepts and facts of the theory without delving into the details of how the concepts and facts were developed. We illustrate the utility of realms through a series of examples. We also give an outline of the mechanisms that are needed to create and maintain realms. △ Less

Submitted 22 May, 2014; originally announced May 2014.

Comments: As accepted for CICM 2014

XLSearch: A Search Engine for Spreadsheets

Authors: Michael Kohlhase, Corneliu Prodescu, Christian Liguda

Abstract: Spreadsheets are end-user programs and domain models that are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. As a result, institutions are swamped by millions of spreadsheets that are becoming increasingly difficult to manage, access, and control. This note presents the XLSearch system, a… ▽ More Spreadsheets are end-user programs and domain models that are heavily employed in administration, financial forecasting, education, and science because of their intuitive, flexible, and direct approach to computation. As a result, institutions are swamped by millions of spreadsheets that are becoming increasingly difficult to manage, access, and control. This note presents the XLSearch system, a novel search engine for spreadsheets. It indexes spreadsheet formulae and efficiently answers formula queries via unification (a complex query language that allows metavariables in both the query as well as the index). But a web-based search engine is only one application of the underlying technology: Spreadsheet formula export to web standards like MathML combined with formula indexing can be used to find similar spreadsheets or common formula errors. △ Less

Submitted 28 January, 2014; originally announced January 2014.

Comments: 12 Pages. 10 B&W & Colour Figures. Proc. European Spreadsheet Risks Int. Grp. (EuSpRIG) 2013, ISBN: 978-1-9054045-1-3

Towards Ontological Support for Principle Solutions in Mechanical Engineering

Authors: Thilo Breitsprecher, Mihai Codescu, Constantin Jucovschi, Michael Kohlhase, Lutz Schröder, Sandro Wartzack

Abstract: The engineering design process follows a series of standardized stages of development, which have many aspects in common with software engineering. Among these stages, the principle solution can be regarded as an analogue of the design specification, fixing as it does the way the final product works. It is usually constructed as an abstract sketch (hand-drawn or constructed with a CAD system) wher… ▽ More The engineering design process follows a series of standardized stages of development, which have many aspects in common with software engineering. Among these stages, the principle solution can be regarded as an analogue of the design specification, fixing as it does the way the final product works. It is usually constructed as an abstract sketch (hand-drawn or constructed with a CAD system) where the functional parts of the product are identified, and geometric and topological constraints are formulated. Here, we outline a semantic approach where the principle solution is annotated with ontological assertions, thus making the intended requirements explicit and available for further machine processing; this includes the automated detection of design errors in the final CAD model, making additional use of a background ontology of engineering knowledge. We embed this approach into a document-oriented design workflow, in which the background ontology and semantic annotations in the documents are exploited to trace parts and requirements through the design process and across different applications. △ Less

Submitted 12 December, 2013; v1 submitted 9 December, 2013; originally announced December 2013.

A Universal Machine for Biform Theory Graphs

Authors: Michael Kohlhase, Felix Mance, Florian Rabe

Abstract: Broadly speaking, there are two kinds of semantics-aware assistant systems for mathematics: proof assistants express the semantic in logic and emphasize deduction, and computer algebra systems express the semantics in programming languages and emphasize computation. Combining the complementary strengths of both approaches while mending their complementary weaknesses has been an important goal of t… ▽ More Broadly speaking, there are two kinds of semantics-aware assistant systems for mathematics: proof assistants express the semantic in logic and emphasize deduction, and computer algebra systems express the semantics in programming languages and emphasize computation. Combining the complementary strengths of both approaches while mending their complementary weaknesses has been an important goal of the mechanized mathematics community for some time. We pick up on the idea of biform theories and interpret it in the MMTt/OMDoc framework which introduced the foundations-as-theories approach, and can thus represent both logics and programming languages as theories. This yields a formal, modular framework of biform theory graphs which mixes specifications and implementations sharing the module system and ty** information. We present automated knowledge management work flows that interface to existing specification/programming tools and enable an OpenMath Machine, that operationalizes biform theories, evaluating expressions by exhaustively applying the implementations of the respective operators. We evaluate the new biform framework by adding implementations to the OpenMath standard content dictionaries. △ Less

Submitted 13 June, 2013; originally announced June 2013.

Comments: Conferences on Intelligent Computer Mathematics, CICM 2013 The final publication is available at http://link.springer.com/

The Planetary Project: Towards eMath3.0

Authors: Michael Kohlhase

Abstract: The Planetary project develops a general framework - the Planetary system - for social semantic portals that support users in interacting with STEM (Science/Technology/Engineering/Mathematics) documents. Developed from an initial attempt to replace the aging portal of PlanetMath.org with a mashup of existing MKM technologies, the Planetary system is now in a state, where it can serve as a basis fo… ▽ More The Planetary project develops a general framework - the Planetary system - for social semantic portals that support users in interacting with STEM (Science/Technology/Engineering/Mathematics) documents. Developed from an initial attempt to replace the aging portal of PlanetMath.org with a mashup of existing MKM technologies, the Planetary system is now in a state, where it can serve as a basis for various eMath3.0 portals, ranging from eLearning systems over scientific archives to semantic help systems. △ Less

Submitted 21 June, 2012; originally announced June 2012.

Comments: Intelligent Computer Mathematics, Johan Jeuring, John A. Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel, and Volker Sorge, eds, Springer Verlag LNAI 7362, 2012

Reimplementing the Mathematical Subject Classification (MSC) as a Linked Open Dataset

Authors: Christoph Lange, Patrick Ion, Anastasia Dimou, Charalampos Bratsas, Joseph Corneli, Wolfram Sperber, Michael Kohlhase, Ioannis Antoniou

Abstract: The Mathematics Subject Classification (MSC) is a widely used scheme for classifying documents in mathematics by subject. Its traditional, idiosyncratic conceptualization and representation makes the scheme hard to maintain and requires custom implementations of search, query and annotation support. This limits uptake e.g. in semantic web technologies in general and the creation and exploration of… ▽ More The Mathematics Subject Classification (MSC) is a widely used scheme for classifying documents in mathematics by subject. Its traditional, idiosyncratic conceptualization and representation makes the scheme hard to maintain and requires custom implementations of search, query and annotation support. This limits uptake e.g. in semantic web technologies in general and the creation and exploration of connections between mathematics and related domains (e.g. science) in particular. This paper presents the new official implementation of the MSC2010 as a Linked Open Dataset, building on SKOS (Simple Knowledge Organization System). We provide a brief overview of the dataset's structure, its available implementations, and first applications. △ Less

Submitted 23 April, 2012; originally announced April 2012.

Comments: Conference on Intelligent Computer Mathematics, July 9-14, Bremen, Germany. Published as number 7362 in Lecture Notes in Artificial Intelligence, Springer

MSC Class: 68T30 ACM Class: H.3.5; I.2.4; J.2

Licensing the Mizar Mathematical Library

Authors: Jesse Alama, Michael Kohlhase, Adam Naumowicz, Piotr Rudnicki, Josef Urban, Lionel Mamane

Abstract: The Mizar Mathematical Library (MML) is a large corpus of formalised mathematical knowledge. It has been constructed over the course of many years by a large number of authors and maintainers. Yet the legal status of these efforts of the Mizar community has never been clarified. In 2010, after many years of loose deliberations, the community decided to investigate the issue of licensing the conten… ▽ More The Mizar Mathematical Library (MML) is a large corpus of formalised mathematical knowledge. It has been constructed over the course of many years by a large number of authors and maintainers. Yet the legal status of these efforts of the Mizar community has never been clarified. In 2010, after many years of loose deliberations, the community decided to investigate the issue of licensing the content of the MML, thereby clarifying and crystallizing the status of the texts, the text's authors, and the library's long-term maintainers. The community has settled on a copyright and license policy that suits the peculiar features of Mizar and its community. In this paper we discuss the copyright and license solutions. We offer our experience in the hopes that the communities of other libraries of formalised mathematical knowledge might take up the legal and scientific problems that we addressed for Mizar. △ Less

Submitted 16 July, 2011; originally announced July 2011.

Comments: To appear in The Conference of Intelligent Computer Mathematics: CICM 2011

Journal ref: Intelligent Computer Mathematics 2011, LNCS 6824, pp. 133-148

A Foundational View on Integration Problems

Authors: Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen

Abstract: The integration of reasoning and computation services across system and language boundaries is a challenging problem of computer science. In this paper, we use integration for the scenario where we have two systems that we integrate by moving problems and solutions between them. While this scenario is often approached from an engineering perspective, we take a foundational view. Based on the gener… ▽ More The integration of reasoning and computation services across system and language boundaries is a challenging problem of computer science. In this paper, we use integration for the scenario where we have two systems that we integrate by moving problems and solutions between them. While this scenario is often approached from an engineering perspective, we take a foundational view. Based on the generic declarative language MMT, we develop a theoretical framework for system integration using theories and partial theory morphisms. Because MMT permits representations of the meta-logical foundations themselves, this includes integration across logics. We discuss safe and unsafe integration schemes and devise a general form of safe integration. △ Less

Submitted 13 May, 2011; originally announced May 2011.

Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics

Authors: Serge Autexier, Catalin David, Dominik Dietrich, Michael Kohlhase, Vyacheslav Zholudev

Abstract: Mathematical knowledge is a central component in science, engineering, and technology (documentation). Most of it is represented informally, and -- in contrast to published research mathematics -- subject to continual change. Unfortunately, machine support for change management has either been very coarse grained and thus barely useful, or restricted to formal languages, where automation is possib… ▽ More Mathematical knowledge is a central component in science, engineering, and technology (documentation). Most of it is represented informally, and -- in contrast to published research mathematics -- subject to continual change. Unfortunately, machine support for change management has either been very coarse grained and thus barely useful, or restricted to formal languages, where automation is possible. In this paper, we report on an effort to extend change management to collections of semi-formal documents which flexibly intermix mathematical formulas and natural language and to integrate it into a semantic publishing system for mathematical knowledge. We validate the long-standing assumption that the semantic annotations in these flexiformal documents that drive the machine-supported interaction with documents can support semantic impact analyses at the same time. But in contrast to the fully formal setting, where adaptations of impacted documents can be automated to some degree, the flexiformal setting requires much more user interaction and thus a much tighter integration into document management workflows. △ Less

Submitted 12 May, 2011; originally announced May 2011.

Comments: 16 pages, Conference on Intelligent Computer Mathematics 2011, July, Bertinoro, Italy

MSC Class: 68U35 ACM Class: E.2; H.3.7; H.3.6; G.4; F.4.2

A Scalable Module System

Authors: Florian Rabe, Michael Kohlhase

Abstract: Symbolic and logic computation systems ranging from computer algebra systems to theorem provers are finding their way into science, technology, mathematics and engineering. But such systems rely on explicitly or implicitly represented mathematical knowledge that needs to be managed to use such systems effectively. While mathematical knowledge management (MKM) "in the small" is well-studied, scal… ▽ More Symbolic and logic computation systems ranging from computer algebra systems to theorem provers are finding their way into science, technology, mathematics and engineering. But such systems rely on explicitly or implicitly represented mathematical knowledge that needs to be managed to use such systems effectively. While mathematical knowledge management (MKM) "in the small" is well-studied, scaling up to large, highly interconnected corpora remains difficult. We hold that in order to realize MKM "in the large", we need representation languages and software architectures that are designed systematically with large-scale processing in mind. Therefore, we have designed and implemented the MMT language -- a module system for mathematical theories. MMT is designed as the simplest possible language that combines a module system, a foundationally uncommitted formal semantics, and web-scalable implementations. Due to a careful choice of representational primitives, MMT allows us to integrate existing representation languages for formal mathematical knowledge in a simple, scalable formalism. In particular, MMT abstracts from the underlying mathematical and logical foundations so that it can serve as a standardized representation format for a formal digital library. Moreover, MMT systematically separates logic-dependent and logic-independent concerns so that it can serve as an interface layer between computation systems and MKM systems. △ Less

Submitted 3 May, 2011; originally announced May 2011.

Comments: This is a preprint of the main paper on the MMT language

The Planetary System: Executable Science, Technology, Engineering and Math Papers

Authors: Christoph Lange, Michael Kohlhase, Catalin David, Deyan Ginev, Andrea Kohlhase, Bogdan Matican, Stefan Mirea, Vyacheslav Zholudev

Abstract: Executable scientific papers contain not just layouted text for reading. They contain, or link to, machine-comprehensible representations of the scientific findings or experiments they describe. Client-side players can thus enable readers to "check, manipulate and explore the result space". We have realized executable papers in the STEM domain with the Planetary system. Semantic annotations associ… ▽ More Executable scientific papers contain not just layouted text for reading. They contain, or link to, machine-comprehensible representations of the scientific findings or experiments they describe. Client-side players can thus enable readers to "check, manipulate and explore the result space". We have realized executable papers in the STEM domain with the Planetary system. Semantic annotations associate the papers with a content commons holding the background ontology, the annotations are exposed as Linked Data, and a frontend player application hooks modular interactive services into the semantic annotations. △ Less

Submitted 8 March, 2011; originally announced March 2011.

Comments: Extended Semantic Web Conference (ESWC 2011), Demo Track. To be published in the Springer LNCS series

MSC Class: 68T35 ACM Class: H.3.5; I.2.1; I.2.6; I.7.1; I.7.2; J.2; K.4.3

What we understand is what we get: Assessment in Spreadsheets

Authors: Andrea Kohlhase, Michael Kohlhase

Abstract: In previous work we have studied how an explicit representation of background knowledge associated with a specific spreadsheet can be exploited to alleviate usability problems with spreadsheet-based applications. We have implemented this approach in the SACHS system to provide a semantic help system for spreadsheets applications. In this paper, we evaluate the (comprehension) coverage of SACHS on… ▽ More In previous work we have studied how an explicit representation of background knowledge associated with a specific spreadsheet can be exploited to alleviate usability problems with spreadsheet-based applications. We have implemented this approach in the SACHS system to provide a semantic help system for spreadsheets applications. In this paper, we evaluate the (comprehension) coverage of SACHS on an Excel-based financial controlling system via a "Wizard-of-Oz" experiment. This shows that SACHS adds significant value, but systematically misses important classes of explanations. For judgements about the information contained in spreadsheets, we provide a first approach for an "assessment module" in SACHS. △ Less

Submitted 14 September, 2010; originally announced September 2010.

Comments: 11 Pages, 10 Colour Figures

Journal ref: Proc. European Spreadsheet Risks Int. Grp. (EuSpRIG) 2010 111-122 ISBN 978-1-905404-50-6

sTeX+ - a System for Flexible Formalization of Linked Data

Authors: Andrea Kohlhase, Michael Kohlhase, Christoph Lange

Abstract: We present the sTeX+ system, a user-driven advancement of sTeX - a semantic extension of LaTeX that allows for producing high-quality PDF documents for (proof)reading and printing, as well as semantic XML/OMDoc documents for the Web or further processing. Originally sTeX had been created as an invasive, semantic frontend for authoring XML documents. Here, we used sTeX in a Software Engineering cas… ▽ More We present the sTeX+ system, a user-driven advancement of sTeX - a semantic extension of LaTeX that allows for producing high-quality PDF documents for (proof)reading and printing, as well as semantic XML/OMDoc documents for the Web or further processing. Originally sTeX had been created as an invasive, semantic frontend for authoring XML documents. Here, we used sTeX in a Software Engineering case study as a formalization tool. In order to deal with modular pre-semantic vocabularies and relations, we upgraded it to sTeX+ in a participatory design process. We present a tool chain that starts with an sTeX+ editor and ultimately serves the generated documents as XHTML+RDFa Linked Data via an OMDoc-enabled, versioned XML database. In the final output, all structural annotations are preserved in order to enable semantic information retrieval services. △ Less

Submitted 23 June, 2010; originally announced June 2010.

Comments: I-SEMANTICS 2010, September 1-3, 2010, Graz, Austria

MSC Class: 68T35; 68T30 ACM Class: H.5.3; H.5.4; I.7.2; F.4.m; H.3.5; D.2.1; D.2.7; I.2.4; K.6.3

sTeXIDE: An Integrated Development Environment for sTeX Collections

Authors: Constantin Jucovschi, Michael Kohlhase

Abstract: Authoring documents in MKM formats like OMDoc is a very tedious task. After years of working on a semantically annotated corpus of sTeX documents (GenCS), we identified a set of common, time-consuming subtasks, which can be supported in an integrated authoring environment. We have adapted the modular Eclipse IDE into sTeXIDE, an authoring solution for enhancing productivity in contributing to sTeX… ▽ More Authoring documents in MKM formats like OMDoc is a very tedious task. After years of working on a semantically annotated corpus of sTeX documents (GenCS), we identified a set of common, time-consuming subtasks, which can be supported in an integrated authoring environment. We have adapted the modular Eclipse IDE into sTeXIDE, an authoring solution for enhancing productivity in contributing to sTeX based corpora. sTeXIDE supports context-aware command completion, module management, semantic macro retrieval, and theory graph navigation. △ Less

Submitted 29 May, 2010; originally announced May 2010.

Comments: To appear in The 9th International Conference on Mathematical Knowledge Management: MKM 2010

Towards MKM in the Large: Modular Representation and Scalable Software Architecture

Authors: Michael Kohlhase, Florian Rabe, Vyacheslav Zholudev

Abstract: MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM "in the small" is well-studied, so the real problem is to scale up to large, highly interconnected corpora: "MKM in the large". We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need… ▽ More MKM has been defined as the quest for technologies to manage mathematical knowledge. MKM "in the small" is well-studied, so the real problem is to scale up to large, highly interconnected corpora: "MKM in the large". We contend that advances in two areas are needed to reach this goal. We need representation languages that support incremental processing of all primitive MKM operations, and we need software architectures and implementations that implement these operations scalably on large knowledge bases. We present instances of both in this paper: the MMT framework for modular theory-graphs that integrates meta-logical foundations, which forms the base of the next OMDoc version; and TNTBase, a versioned storage system for XML-based document formats. TNTBase becomes an MMT database by instantiating it with special MKM operations for MMT. △ Less

Submitted 31 May, 2010; v1 submitted 28 May, 2010; originally announced May 2010.

Comments: To appear in The 9th International Conference on Mathematical Knowledge Management: MKM 2010

Dimensions of Formality: A Case Study for MKM in Software Engineering

Authors: Andrea Kohlhase, Michael Kohlhase, Christoph Lange

Abstract: We study the formalization of a collection of documents created for a Software Engineering project from an MKM perspective. We analyze how document and collection markup formats can cope with an open-ended, multi-dimensional space of primary and secondary classifications and relationships. We show that RDFa-based extensions of MKM formats, employing flexible "metadata" relationships referencing sp… ▽ More We study the formalization of a collection of documents created for a Software Engineering project from an MKM perspective. We analyze how document and collection markup formats can cope with an open-ended, multi-dimensional space of primary and secondary classifications and relationships. We show that RDFa-based extensions of MKM formats, employing flexible "metadata" relationships referencing specific vocabularies for distinct dimensions, are well-suited to encode this and to put it into service. This formalized knowledge can be used for enriching interactive document browsing, for enabling multi-dimensional metadata queries over documents and collections, and for exporting Linked Data to the Semantic Web and thus enabling further reuse. △ Less

Submitted 28 April, 2010; originally announced April 2010.

Comments: To appear in The 9th International Conference on Mathematical Knowledge Management: MKM 2010

MSC Class: 68T35; 68T30 ACM Class: H.5.3; H.5.4; I.7.2; F.4.m; H.3.5; D.2.7; I.2.4; K.6.3

Publishing Math Lecture Notes as Linked Data

Authors: Catalin David, Michael Kohlhase, Christoph Lange, Florian Rabe, Nikita Zhiltsov, Vyacheslav Zholudev

Abstract: We mark up a corpus of LaTeX lecture notes semantically and expose them as Linked Data in XHTML+MathML+RDFa. Our application makes the resulting documents interactively browsable for students. Our ontology helps to answer queries from students and lecturers, and paves the path towards an integration of our corpus with external sites. We mark up a corpus of LaTeX lecture notes semantically and expose them as Linked Data in XHTML+MathML+RDFa. Our application makes the resulting documents interactively browsable for students. Our ontology helps to answer queries from students and lecturers, and paves the path towards an integration of our corpus with external sites. △ Less

Submitted 20 April, 2010; originally announced April 2010.

Comments: 7th Extended Semantic Web Conference (http://www.eswc2010.org), Demo Track

MSC Class: 68T35; 68T30 ACM Class: H.2.4; H.2.8; H.3.5; G.4; F.4.m; H.5.3; H.5.4; J.2

Cut-Simulation and Impredicativity

Authors: Christoph Benzmueller, Chad E. Brown, Michael Kohlhase

Abstract: We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for classical type theory -- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and… ▽ More We investigate cut-elimination and cut-simulation in impredicative (higher-order) logics. We illustrate that adding simple axioms such as Leibniz equations to a calculus for an impredicative logic -- in our case a sequent calculus for classical type theory -- is like adding cut. The phenomenon equally applies to prominent axioms like Boolean- and functional extensionality, induction, choice, and description. This calls for the development of calculi where these principles are built-in instead of being treated axiomatically. △ Less

Submitted 2 March, 2009; v1 submitted 30 January, 2009; originally announced February 2009.

Comments: 21 pages

ACM Class: F.4.1; I.2.3

Journal ref: Logical Methods in Computer Science, Volume 5, Issue 1 (March 3, 2009) lmcs:1144

Computing Parallelism in Discourse

Authors: Claire Gardent, Michael Kohlhase

Abstract: Although much has been said about parallelism in discourse, a formal, computational theory of parallelism structure is still outstanding. In this paper, we present a theory which given two parallel utterances predicts which are the parallel elements. The theory consists of a sorted, higher-order abductive calculus and we show that it reconciles the insights of discourse theories of parallelism w… ▽ More Although much has been said about parallelism in discourse, a formal, computational theory of parallelism structure is still outstanding. In this paper, we present a theory which given two parallel utterances predicts which are the parallel elements. The theory consists of a sorted, higher-order abductive calculus and we show that it reconciles the insights of discourse theories of parallelism with those of Higher-Order Unification approaches to discourse semantics, thereby providing a natural framework in which to capture the effect of parallelism on discourse semantics. △ Less

Submitted 1 May, 1997; originally announced May 1997.

Comments: 6 pages

Report number: CLAUS Nr. 90

Journal ref: Proceedings of IJCAI'97

Corrections and Higher-Order Unification

Authors: Claire Gardent, Michael Kohlhase, Noor van Neusen

Abstract: We propose an analysis of corrections which models some of the requirements corrections place on context. We then show that this analysis naturally extends to the interaction of corrections with pronominal anaphora on the one hand, and (in)definiteness on the other. The analysis builds on previous unification--based approaches to NL semantics and relies on Higher--Order Unification with Equivale… ▽ More We propose an analysis of corrections which models some of the requirements corrections place on context. We then show that this analysis naturally extends to the interaction of corrections with pronominal anaphora on the one hand, and (in)definiteness on the other. The analysis builds on previous unification--based approaches to NL semantics and relies on Higher--Order Unification with Equivalences, a form of unification which takes into account not only syntactic beta-eta-identity but also denotational equivalence. △ Less

Submitted 2 September, 1996; originally announced September 1996.

Comments: 12 pages, LateX file, In Proccedings of the 3. Konferenz zur Verarbeitung natuerlicher Sprache (KONVENS), Bielefeld, 1996

Report number: CLAUS Report Nr. 77

Focus and Higher-Order Unification

Authors: Claire Gardent, Michael Kohlhase

Abstract: Pulman has shown that Higher--Order Unification (HOU) can be used to model the interpretation of focus. In this paper, we extend the unification--based approach to cases which are often seen as a test--bed for focus theory: utterances with multiple focus operators and second occurrence expressions. We then show that the resulting analysis favourably compares with two prominent theories of focus… ▽ More Pulman has shown that Higher--Order Unification (HOU) can be used to model the interpretation of focus. In this paper, we extend the unification--based approach to cases which are often seen as a test--bed for focus theory: utterances with multiple focus operators and second occurrence expressions. We then show that the resulting analysis favourably compares with two prominent theories of focus (namely, Rooth's Alternative Semantics and Krifka's Structured Meanings theory) in that it correctly generates interpretations which these alternative theories cannot yield. Finally, we discuss the formal properties of the approach and argue that even though HOU need not terminate, for the class of unification--problems dealt with in this paper, HOU avoids this shortcoming and is in fact computationally tractable. △ Less

Submitted 2 May, 1996; originally announced May 1996.

Comments: 6 pages, Latex file, uses colap.sty, to appear in Proceedings of COLING 96

Report number: CLAUS-75

Higher-Order Coloured Unification and Natural Language Semantics

Authors: Claire Gardent, Michael Kohlhase

Abstract: In this paper, we show that Higher-Order Coloured Unification - a form of unification developed for automated theorem proving - provides a general theory for modeling the interface between the interpretation process and other sources of linguistic, non semantic information. In particular, it provides the general theory for the Primary Occurrence Restriction which (Dalrymple, Shieber and Pereira,… ▽ More In this paper, we show that Higher-Order Coloured Unification - a form of unification developed for automated theorem proving - provides a general theory for modeling the interface between the interpretation process and other sources of linguistic, non semantic information. In particular, it provides the general theory for the Primary Occurrence Restriction which (Dalrymple, Shieber and Pereira, 1991)'s analysis called for. △ Less

Submitted 2 May, 1996; originally announced May 1996.

Comments: 9 pages, LateX file, uses aclap.sty, To appear in Proceedings of ACL96

Report number: CLAUS-76