activity
19962020
most citedLicensing the Mizar Mathematical Library

31 citations · 149 across the 30 of their papers we have counts for

collaborators

32 papers

cs.LO2020

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…

cs.LO2020

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…

cs.LO2020

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…

cs.MS2020★ 2 cited

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

Katja Bercic, Jacques Carette, William M. Farmer +4

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 mathemati…

cs.CL2019★ 4 cited

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

Michael Kohlhase, Jan Frederik Schaefer

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 i…

cs.HC2019★ 1 cited

TGView3D System Description: 3-Dimensional Visualization of Theory Graphs

Richard Marcus, Michael Kohlhase, Florian Rabe

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 hiera…