BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Michael Kohlhase

Michael Kohlhase appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Digital LibrariesLogic in Computer ScienceMathematical SoftwareSoftware EngineeringArtificial IntelligenceDatabasesHuman-Computer Interactionmath.HOOther Computer Science

Catalog footprint

What is connected

21works
9topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

21 published item(s)

preprint2020arXiv

Context Graphs for Legal Reasoning and Argumentation

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Experiences from Exporting Major Proof Assistant Libraries

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Making Isabelle Content Accessible in Knowledge Representation Formats

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Realms: A Structure for Consolidating Knowledge about Mathematical Theories

Since there are different ways of axiomatizing and developing 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.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

XLSearch: A Search Engine for Spreadsheets

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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

A Universal Machine for Biform Theory Graphs

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 typing 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.

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

Towards Ontological Support for Principle Solutions in Mechanical Engineering

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2012arXiv

The Planetary Project: Towards eMath3.0

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.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

A Foundational View on Integration Problems

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.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

A Scalable Module System

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.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

Licensing the Mizar Mathematical Library

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.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2011arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

sTeX+ - a System for Flexible Formalization of Linked Data

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.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

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

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.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

What we understand is what we get: Assessment in Spreadsheets

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.

0 citations0 reviewsNo code linkedOpen access