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
• 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