Michael Kohlhase: Selected Publications
(please respect possibly existing copyrights when copying)
- MBase/OMDoc (see the web pages mbase,omdoc))
- Towards Collaborative Content Management And Version Control For Structured Mathematical Knowledge, with Romeo Anghelache, Mathematical Knowledge Management (MKM 2003)
- System Description: MBase, an Open Mathematical Knowledge Base, with Andreas Franke, CADE-17, Pittsburgh
- MBase: Representing Knowledge and Context for the Integration of Mathematical Software Systems, with Andreas Franke, to appear in Journal of Symbolic Computation.
- OMDoc: An Infrastructure for OpenMath Content Dictionary Information Bulletin of the ACM SIGSAM, 2000.
-
Towards an Internet Standard for the Administration, Distribution and
Teaching of mathematical Knowledge AISC'00, 2000.
(Long version appeared as Seki Report SR-00-02)
-
Higher-Order Unification
(for applications see HO-ATP or NL sections)
- Unification in a lambda-Calculus with Intersection Types, with Frank Pfenning, International Logic Programming Symposion 1993, Vancouver Canada
- Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading with Patricia Johann, CADE'94, Nancy, France.
- Unification in a lambda-Calculus with Term Declarations and Function Sorts Annual German Conference on Artificial Intelligence KI'94, Saarbrücken, Germany
- A Colored Version of the lambda-Calculus, with Dieter Hutter, CADE-14 Townsville, Australia, 1997.
- Managing Structural Information by Higher-Order Colored Unification, with Dieter Hutter, Journal of Automated Reasoning 25:2, 2000.
- Higher-Order Theorem Proving
- Model Existence for Higher Order Logic: Journal of Symbolic Logic 69:4 (2004), with Christoph Benzmüller.
- Higher-Order Tableaux Tableau Workshop 1995, Koblenz, Germany
-
Extensional Higher-Order Resolution,
with
Christoph Benzmüller CADE'98
(see also Seki Report SR-97-10 ). - Higher-Order Automated Theorem Proving, in Bibel and Schmitt (eds.) "Deduction - A basis for Applications" Kluwer, 1998.
- LEO -- A Higher-Order Theorem Prover , with Christoph Benzmüller in CADE'98.
- Deduction with Partial Functions/multiple Truth values
- A Mechanization of B Kleene Logic for Partial Functions, with Manfred Kerber; CADE'94, Nancy, France.
- A Tableau Calculus for Partial Functions with Manfred Kerber, Annals of the Kurt Gödel Society.
- A Resolution Calculus for Presuppositions with Manfred Kerber, Proc ECAI'96
- Mechanising Partiality without Re-Implementation with Manfred Kerber, Proc KI'97
- Higher-Order Multi-Valued Resolution with Ortwin Scheja Journal of Applied Non-Classical Logic 9:4, 1999.
- Deduction Systems
- General/Philosophy
- Guaranteeing Correctness through the Communication of Checkable Proofs (or: Would You Really Trust an Automated Reasoning System?) with The OMEGA group CADE-Workshop 1994.
- A Test for Evaluating the Practical Usefulness of Deduction Systems with the OMEGA Group, CADE Workshop 1994.
- Proof Planning
- Adapting Methods to Novel Tasks in Proof Planning with Xiaorong Huang, Manfred Kerber, and Jörn Richts, Annual German Conference on Artificial Intelligence KI'94, Saarbrücken, Germany
- The OMEGA System
- OMEGA: Ein mathematisches Assistenzsystem, Kognitionswissenschaft, with Jörg Siekmann and Erica Melis
- KEIM: A Toolkit for Automated Deduction with The OMEGA group, CADE 1994.
- OMEGA-MKRP: A proof development environment with The OMEGA group, CADE 1994.
- OMEGA: Towards a Mathematical Assistant with The OMEGA group CADE 1997.
- Integration of Inference Systems
- LOUI: Lovely OMEGA User Interface, whith the OMEGA group, Formal Aspects of Computing 11, pp. 326-342, 1999.
- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving, CADE'99 with Andreas Franke
- Agent-Oriented Integration of Distributed Mathematical Services, Journal of Universal Computer Science 5:3, with Andreas Franke, Stephan Hess, Christoph Jung, and Volker Sorge.
- Integrating Computer Algebra into Proof Planning with Manfred Kerber and Volker Sorge Journal of Automated Reasoning 21(3) 1998.
- Communication Protocols for Mathematical Services based on KQML and OMRS. Proceedings of the Calculemus Symposium. (in press), with Alessandro Armando and Silvio Ranise
- General/Philosophy
- Natural Language Semantics
- Feature Logic for Dotted Types: A Formalism for Complex Word Meanings with Manfred Pinkal ACL-2000, Honkong.
- Resource-Adaptive Model Generation as a Performance Model with Alexander KollerLogic Journal of the IGPL 11:4 (2003).
- Model Generation for Discourse Representation Theory, ECAI 2000.
- Higher-Order Coloured Unification: A linguistic Application Techniques and Sciences Informatiques 13:3, 1-33, with Claire Gardent and Karsten Konrad.
- Inference and Computational Semantics with Patrick Blackburn and Johan Bos and Hans de Nivelle IWCS III (Third International Workshop on Computational Semantics), Tilburg, 1999.
- Steuerung der Inferenz in der Diskursverarbeitung with Claire Gardent and Markus Egg Kognitionswissenschaft.
- Computing parallelism in discourse with Claire Gardent Proc IJCAI'97.
- Higher-Order Coloured Unification and Natural Language Semantics with Claire Gardent, Proc. ACL 1996.
- Focus and Higher-Order Unification with Claire Gardent Proc. COliNG'96.
- Corrections and higher-order unification with Claire Gardent and Noor van Leusen, Proc. KONVENS'96.
- A type-theoretic semantics for lambda-DRT with Susanna Kuschert and Manfred Pinkal, Tenth Amsterdam Koolloquim.
-
Theses
- Masters thesis: "Eine hinreichende Bedingung für die starke, homologische Minimalität von kompakten, F-extremalen Hyperflächen in glatten Mannigfaltigkeiten". University of Bonn, Germany, October 1989.
- A Mechanization of Sorted Higher-Order Logic Based on the Resolution Principle Phd-thesis 1994, Universität des Saarlandes, Germany