31 citations · 149 across the 30 of their papers we have counts for
8 papers · 1 filter
Context Graphs for Legal Reasoning and Argumentation
Max Rapp, Axel Adrian, Michael Kohlhase
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 a…
Making Isabelle Content Accessible in Knowledge Representation Formats
Michael Kohlhase, Florian Rabe, Makarius Wenzel
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 adeq…
Experiences from Exporting Major Proof Assistant Libraries
Michael Kohlhase, Florian Rabe
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 previ…
The Theorem Prover Museum -- Conserving the System Heritage of Automated Reasoning
Michael Kohlhase
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…
A Universal Machine for Biform Theory Graphs
Michael Kohlhase, Felix Mance, Florian Rabe
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 alg…
A Foundational View on Integration Problems
Florian Rabe, Michael Kohlhase, Claudio Sacerdoti Coen
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…