Michael Kohlhase

According to our database1, Michael Kohlhase authored at least 167 papers between 1992 and 2019.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Homepages:

On csauthors.net:

Bibliography

2019
Relational Data Across Mathematical Libraries.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

Towards a Unified Mathematical Data Infrastructure: Database and Interface Generation.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

Integrating Semantic Mathematical Documents and Dynamic Notebooks.
Proceedings of the Intelligent Computer Mathematics - 12th International Conference, 2019

2018
A Proposal for an OpenMath JSON Encoding.
Proceedings of the Joint Proceedings of the CME-EI, 2018

Syntactic/Semantic Analysis for High-Precision Math Linguistics (short paper).
Proceedings of the Joint Proceedings of the CME-EI, 2018

Knowledge Amalgamation for Computational Science and Engineering.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Automatically Finding Theory Morphisms for Knowledge Management.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Discourse Phenomena in Mathematical Documents.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Translating the IMPS Theory Library to MMT/OMDoc.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2018

Towards Context Graphs for Argumentation Logics.
Proceedings of the Conference "Lernen, Wissen, Daten, Analysen", 2018

Theories as Types.
Proceedings of the Automated Reasoning - 9th International Joint Conference, 2018

2017
Classification of Alignments Between Concepts of Formal Mathematical Systems.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Software Citations, Information Systems, and Beyond.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Mathematical Models as Research Data via Flexiformal Theory Graphs.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Visual Structure in Mathematical Expressions.
Proceedings of the Intelligent Computer Mathematics - 10th International Conference, 2017

Virtual Theories - A Uniform Interface to Mathematical Knowledge Bases.
Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2017

Knowledge-Based Interoperability for Mathematical Software Systems.
Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2017

Math Object Identifiers - Towards Research Data in Mathematics.
Proceedings of the Lernen, 2017

Making PVS Accessible to Generic Services by Interpretation in a Universal Format.
Proceedings of the Interactive Theorem Proving - 8th International Conference, 2017

2016
QED Reloaded: Towards a Pluralistic Formal Library of Mathematical Knowledge.
J. Formalized Reasoning, 2016

NTCIR-12 MathIR Task Overview.
Proceedings of the 12th NTCIR Conference on Evaluation of Information Access Technologies, 2016

Interoperability in the OpenDreamKit Project: The Math-in-the-Middle Approach.
Proceedings of the Intelligent Computer Mathematics - 9th International Conference, 2016

Formula Semantification and Automated Relation Finding in the On-Line Encyclopedia for Integer Sequences.
Proceedings of the Mathematical Software - ICMS 2016, 2016

The SMGloM Project and System: Towards a Terminology and Ontology for Mathematics.
Proceedings of the Mathematical Software - ICMS 2016, 2016

Notation-based Semantification.
Proceedings of the Joint Proceedings of the FM4M, 2016

FrameIT Reloaded: Serious Math Games from Modular Math Ontologies.
Proceedings of the Joint Proceedings of the FM4M, 2016

A Standard for Aligning Mathematical Concepts.
Proceedings of the Joint Proceedings of the FM4M, 2016

2015
Math Literate Knowledge Management via Induced Material.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

A Flexiformal Model of Knowledge Dissemination and Aggregation in Mathematics.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2015

Faceted Search for Mathematics.
Proceedings of the Mathematical Aspects of Computer and Information Sciences, 2015

Importing the OEIS Library Into OMDoc.
Proceedings of the LWA 2015 Workshops: KDML, 2015

Faceted Search for Mathematics.
Proceedings of the LWA 2015 Workshops: KDML, 2015

Assessment for Spreadsheets.
Proceedings of the Second Workshop on Software Engineering Methods in Spreadsheets co-located with the 37th International Conference on Software Engineering (ICSE 2015) , 2015

Context in Spreadsheet Comprehension.
Proceedings of the Second Workshop on Software Engineering Methods in Spreadsheets co-located with the 37th International Conference on Software Engineering (ICSE 2015) , 2015

2014
MathWebSearch at NTCIR-11.
Proceedings of the 11th NTCIR Conference on Evaluation of Information Access Technologies, 2014

NTCIR-11 Math-2 Task Overview.
Proceedings of the 11th NTCIR Conference on Evaluation of Information Access Technologies, 2014

System Description: A Semantics-Aware LaTeX-to-Office Converter.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

OpenMath Language Extensions.
Proceedings of the Joint Proceedings of the MathUI, 2014

Extension Proposal: Records in Pragmatic OpenMath.
Proceedings of the Joint Proceedings of the MathUI, 2014

A Data Model and Encoding for a Semantic, Multilingual Terminology of Mathematics.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

System Description: MathHub.info.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Flexary Operators for Formalized Mathematics.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

Realms: A Structure for Consolidating Knowledge about Mathematical Theories.
Proceedings of the Intelligent Computer Mathematics - International Conference, 2014

OpenMathMap: Interaction.
Proceedings of the Joint Proceedings of the MathUI, 2014

Mathematical Knowledge Management and Information Retrieval: Transcending the One-Brain-Barrier.
Proceedings of the 16th LWA Workshops: KDML, 2014

Discourse-Level Parallel Markup and Meaning Adoption in Flexiformal Theory Graphs.
Proceedings of the Mathematical Software - ICMS 2014, 2014

Representing, Archiving, and Searching the Space of Mathematical Knowledge.
Proceedings of the Mathematical Software - ICMS 2014, 2014

Towards Ontological Support for Principle Solutions in Mechanical Engineering.
Proceedings of the Formal Ontology in Information Systems, 2014

Towards Ontological Support for Principle Solutions in Mechanical Engineering.
Proceedings of the 6th Workshop on Formal Ontologies meet Industry co-located with 8th International Conference on Formal Ontology in Information Systems (FOIS 2014), 2014

2013
The Mizar Mathematical Library in OMDoc: Translation and Applications.
J. Autom. Reasoning, 2013

A scalable module system.
Inf. Comput., 2013

Spreadsheets with a Semantic Layer.
ECEASST, 2013

MathWebSearch at NTCIR-10.
Proceedings of the 10th NTCIR Conference on Evaluation of Information Access Technologies, 2013

NTCIR-10 Math Pilot Task Overview.
Proceedings of the 10th NTCIR Conference on Evaluation of Information Access Technologies, 2013

A Universal Machine for Biform Theory Graphs.
Proceedings of the Intelligent Computer Mathematics, 2013

OpenMathMap: accessing math via interactive maps.
Proceedings of the Joint Proceedings of the MathUI, 2013

OpenMathMap: Accessing Math via Interactive Maps.
Proceedings of the LWA 2013. Lernen, 2013

Full Semantic Transparency: Overcoming Boundaries of Applications.
Proceedings of the Human-Computer Interaction - INTERACT 2013, 2013

2012
Semantics of OpenMath and MathML3.
Mathematics in Computer Science, 2012

Reasoning without believing: on the mechanisation of presuppositions and partiality.
Journal of Applied Non-Classical Logics, 2012

The Flexiformalist Manifesto.
Proceedings of the 14th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, 2012

Bringing Mathematics to the Web of Data: The Case of the Mathematics Subject Classification.
Proceedings of the Semantic Web: Research and Applications, 2012

MathWebSearch 0.5: Scaling an Open Formula Search Engine.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

The Planetary Project: Towards eMath3.0.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

Extending MKM Formats at the Statement Level.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

Semantic Alliance: A Framework for Semantic Allies.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

Reimplementing the Mathematics Subject Classification (MSC) as a Linked Open Dataset.
Proceedings of the Intelligent Computer Mathematics - 11th International Conference, 2012

2011
The Planetary System: Web 3.0 & Active Documents for STEM.
Proceedings of the International Conference on Computational Science, 2011

Towards a flexible notion of document context.
Proceedings of the 29th ACM international conference on Design of communication, 2011

Maintaining islands of consistency via versioned links.
Proceedings of the 29th ACM international conference on Design of communication, 2011

A Foundational View on Integration Problems.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Combining Source, Content, Presentation, Narration, and Relational Representation.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

The LaTeXML Daemon: Editable Math on the Collaborative Web.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Project Abstract: Logic Atlas and Integrator (LATIN).
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Workflows for the Management of Change in Science, Technologies, Engineering and Mathematics.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Licensing the Mizar Mathematical Library.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

MathWebSearch 0.5 An Open Formula Search Engine.
Proceedings of the Report of the symposium "Lernen, 2011

The LaTeXML Daemon: Editable Math on the Collaborative Web.
Proceedings of the Report of the symposium "Lernen, 2011

A Framework for Semantic Publishing of Modular Content Objects.
Proceedings of the 1st Workshop on Semantic Publishing 2011, 2011

The Planetary System: Executable Science, Technology, Engineering and Math Papers.
Proceedings of the Semanic Web: Research and Applications, 2011

2010
Transforming Large Collections of Scientific Publications to XML.
Mathematics in Computer Science, 2010

Towards Logical Frameworks in the Heterogeneous Tool Set Hets.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2010

A Proof Theoretic Interpretation of Model Theoretic Hiding.
Proceedings of the Recent Trends in Algebraic Development Techniques, 2010

Prototyping a Browser for a Listed Buildings Database with Semantic MediaWiki.
Proceedings of the 5th Workshop on Semantic Wikis, 2010

STEX+: a system for flexible formalization of linked data.
Proceedings of the Proceedings the 6th International Conference on Semantic Systems, 2010

Publishing Math Lecture Notes as Linked Data.
Proceedings of the Semantic Web: Research and Applications, 2010

Towards MKM in the Large: Modular Representation and Scalable Software Architecture.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

Dimensions of Formality: A Case Study for MKM in Software Engineering.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

sTeXIIS: An Integrated Development Environment for sTeX Collections.
Proceedings of the Intelligent Computer Mathematics, 10th International Conference, 2010

2009
Applying Semantic Techniques to Search and Analyze Bug Tracking Data.
J. Network Syst. Manage., 2009

Context-Aware Adaptation: A Case Study On Mathematical Notations.
IS Management, 2009

Cut-Simulation and Impredicativity
Logical Methods in Computer Science, 2009

Modeling task experience in user assistance systems.
Proceedings of the 27th Annual International Conference on Design of Communication, 2009

Semantic transparency in user assistance systems.
Proceedings of the 27th Annual International Conference on Design of Communication, 2009

A Mathematical Approach to Ontology Authoring and Documentation.
Proceedings of the Intelligent Computer Mathematics, 2009

Compensating the Computational Bias of Spreadsheets with MKM Techniques.
Proceedings of the Intelligent Computer Mathematics, 2009

Spreadsheet Interaction with Frames: Exploring a Mathematical Practice.
Proceedings of the Intelligent Computer Mathematics, 2009

Unifying Math Ontologies: A Tale of Two Standards.
Proceedings of the Intelligent Computer Mathematics, 2009

What you understand is what you get: Assessment in Spreadsheets.
Proceedings of the LWA 2009: Workshop-Woche: Lernen, 2009

A Mathematical Approach to Ontology Authoring and Documentation.
Proceedings of the LWA 2009: Workshop-Woche: Lernen, 2009

An Architecture for Linguistic and Semantic Analysis on the arXMLiv Corpus.
Proceedings of the Informatik 2009: Im Focus das Leben, 2009

Formal Management of CAD/CAM Processes.
Proceedings of the FM 2009: Formal Methods, 2009

2008
Semantic Knowledge Management for Education.
Proceedings of the IEEE, 2008

Using as a Semantic Markup Format.
Mathematics in Computer Science, 2008

Towards a Community of Practice Toolkit Based on Semantically Marked Up Artifacts.
Proceedings of the Emerging Technologies and Information Systems for the Knowledge Society, 2008

Fine-Granular Version Control & Redundancy Resolution.
Proceedings of the LWA 2008, 2008

Compensating the Semantic Bias of Spreadsheets.
Proceedings of the LWA 2008, 2008

An Exchange Format for Modular Knowledge.
Proceedings of the LPAR 2008 Workshops, 2008

Transforming the arXiv to XML.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

Notations for Living Mathematical Documents.
Proceedings of the Intelligent Computer Mathematics, 9th International Conference, 2008

2007
Extended Formula Normalization for epsilon -Retrieval and Sharing of Mathematical Knowledge.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

Re examining the MKM Value Proposition: From Math Web Search to Math Web Re Search.
Proceedings of the Towards Mechanized Mathematical Assistants, 14th Symposium, 2007

panta rhei.
Proceedings of the LWA 2007: Lernen - Wissen, 2007

Managing Variants in Document Content and Narrative Structures.
Proceedings of the LWA 2007: Lernen - Wissen, 2007

2006
A Semantic Wiki for Mathematical Knowledge Management.
Proceedings of the SemWiki2006, First Workshop on Semantic Wikis, 2006

Communities of Practice in MKM: An Extensional Model.
Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Capturing the Content of Physics: Systems, Observables, and Experiments.
Proceedings of the Mathematical Knowledge Management, 5th International Conference, 2006

Cut-Simulation in Impredicative Logics.
Proceedings of the Automated Reasoning, Third International Joint Conference, 2006

A Search Engine for Mathematical Formulae.
Proceedings of the Artificial Intelligence and Symbolic Computation, 2006

OMDoc - An Open Markup Format for Mathematical Documents [version 1.2].
Lecture Notes in Computer Science 4180, Springer, ISBN: 3-540-37897-9, 2006

2005
An Exploration in the Space of Mathematical Knowledge.
Proceedings of the Mathematical Knowledge Management, 4th International Conference, 2005

2004
Higher-order semantics and extensionality.
J. Symb. Log., 2004

Inference and Computational Semantics.
Journal of Logic, Language and Information, 2004

CPoint: Dissolving the Author's Dilemma.
Proceedings of the Mathematical Knowledge Management, Third International Conference, 2004

2003
Resource-Adaptive Model Generation as a Performance Model.
Logic Journal of the IGPL, 2003

Editorial.
Logic Journal of the IGPL, 2003

Towards Collaborative Content Management and Version Control for Structured Mathematical Knowledge.
Proceedings of the Mathematical Knowledge Management, Second International Conference, 2003

2002
System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning.
Proceedings of the Automated Deduction, 2002


2001
MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems.
J. Symb. Comput., 2001

2000
Managing Structural Information by Higher-Order Colored Unification.
J. Autom. Reasoning, 2000

OMDoc: an infrastructure for OpenMath content dictionary information.
ACM SIGSAM Bulletin, 2000

System Description: MBASE, an Open Mathematical Knowledge Base.
Proceedings of the Automated Deduction, 2000

Using Deduction Techniques for Natural Language Understanding.
Proceedings of the Seventh Workshop on Automated Reasoning, 2000

OMDOC: Towards an Internet Standard for the Administration, Distribution, and Teaching of Mathematical Knowledge.
Proceedings of the Artificial Intelligence and Symbolic Computation, 2000

Feature Logic for Dotted Types: A Formalism for Complex Word Meanings.
Proceedings of the 38th Annual Meeting of the Association for Computational Linguistics, 2000

1999
Agent-Oriented Integration of Distributed Mathematical Services.
J. UCS, 1999

Higher Order Multi-Valued Resolution.
Journal of Applied Non-Classical Logics, 1999

LUI: Lovely MEGA User Interface.
Formal Asp. Comput., 1999

MBase: Representing mathematical knowledge in a relational data base.
Electr. Notes Theor. Comput. Sci., 1999

System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving.
Proceedings of the Automated Deduction, 1999

1998
MEGA: Ein mathematisches Assistenzsystem.
Kognitionswissenschaft, 1998

Steuerung der Inferenz in der Diskursverarbeitung.
Kognitionswissenschaft, 1998

Integrating Computer Algebra into Proof Planning.
J. Autom. Reasoning, 1998

System Description: LEO - A Higher-Order Theorem Prover.
Proceedings of the Automated Deduction, 1998

Extensional Higher-Order Resolution.
Proceedings of the Automated Deduction, 1998

1997
Mechanising Partiality With Re-implementation.
Proceedings of the KI-97: Advances in Artificial Intelligence, 1997

Computing Parallelism in Discourse.
Proceedings of the Fifteenth International Joint Conference on Artificial Intelligence, 1997

A Colored Version of the Lambda-Calculus.
Proceedings of the Automated Deduction, 1997


1996
Sorten für das automatische Beweisen höherer Stufe.
KI, 1996

Die Beweisentwicklungsumgebung Omega-MKRP.
Inform., Forsch. Entwickl., 1996

Corrections and Higher-Order Unification.
Proceedings of the Natural Language Processing and Speech Technology, 1996

A Resolution Calculus for Presuppositions.
Proceedings of the 12th European Conference on Artificial Intelligence, 1996

Integrating Computer Algebra with Proof Planning.
Proceedings of the Design and Implementation of Symbolic Computation Systems, 1996

Focus and Higher-Order Unification.
Proceedings of the 16th International Conference on Computational Linguistics, 1996

Higher-Order Coloured Unification and Natural Language Semantics.
Proceedings of the 34th Annual Meeting of the Association for Computational Linguistics, 1996

1995
Higher-Order Tableaux.
Proceedings of the Theorem Proving with Analytic Tableaux and Related Methods, 1995

1994
A mechanization of sorted higher-order logic based on the resolution principle.
PhD thesis, 1994

Unification in a Sorted Lambda-Calculus with Term Declarations and Function Sorts.
Proceedings of the KI-94: Advances in Artificial Intelligence, 1994

Adapting Methods to Novel Tasks in Proof Planning.
Proceedings of the KI-94: Advances in Artificial Intelligence, 1994

A Mechanization of Strong Kleene Logic for Partial Functions.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

KEIM: A Toolkit for Automated Deduction.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

Omega-MKRP: A Proof Development Environment.
Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993
Unification in a Lambda-Calculus with Intersection Types.
Proceedings of the Logic Programming, 1993

1992
Unification in Order-Sorted Type Theory.
Proceedings of the Logic Programming and Automated Reasoning, 1992


  Loading...