Travelled to:1 × Australia
1 × Canada
1 × Denmark
1 × France
1 × Germany
1 × Italy
1 × The Netherlands
2 × USA
Collaborated with:C.Benzmüller A.Franke M.Kerber J.Zimmer D.Hutter P.Johann F.Pfenning J.H.Siekmann E.Melis X.Huang C.E.Brown D.M.0001 F.Rabe D.Nesmith J.Richts J.Lemburg L.Schröder E.Schulz L.Cheikhrouhou A.Fiedler A.Meier V.Sorge D.Fehrer K.Konrad W.Schaarschmidt V.Brezhnev H.Horacek M.Moschner I.Normann M.Pollet C.Ullrich C.Wirth
Talks about:descript (4) system (4) mathemat (3) calculus (3) order (3) omega (3) extension (2) distribut (2) function (2) theorem (2)
Person: Michael Kohlhase
DBLP: Kohlhase:Michael
Contributed to:
2009
2006
200220001999199819971994
19932018Wrote 16 papers:
- FM-2009-KohlhaseLSS #process
- Formal Management of CAD/CAM Processes (MK, JL, LS, ES), pp. 223–238.
- IJCAR-2006-BenzmullerBK #logic
- Cut-Simulation in Impredicative Logics (CB, CEB, MK), pp. 220–234.
- CADE-2002-SiekmannBBCFFHKMMMNPSUWZ #development #proving
- Proof Development with OMEGA (JHS, CB, VB, LC, AF, AF, HH, MK, AM, EM, MM, IN, MP, VS, CU, CPW, JZ), pp. 144–149.
- CADE-2002-ZimmerK #distributed #reasoning
- System Description: The MathWeb Software Bus for Distributed Mathematical Reasoning (JZ, MK), pp. 139–143.
- CADE-2000-FrankeK #knowledge base
- System Description: MBASE, an Open Mathematical Knowledge Base (AF, MK), pp. 455–459.
- CADE-1999-FrankeK #automation #communication #distributed #proving #theorem proving
- System Description: MathWeb, an Agent-Based Communication Layer for Distributed Automated Theorem Proving (AF, MK), pp. 217–221.
- CADE-1998-BenzmullerK #higher-order
- Extensional Higher-Order Resolution (CB, MK), pp. 56–71.
- CADE-1998-BenzmullerK98a #higher-order #proving #theorem proving
- System Description: LEO — A Higher-Order Theorem Prover (CB, MK), pp. 139–144.
- CADE-1997-BenzmullerCFFHKKKMMSSS #named #towards
- Omega: Towards a Mathematical Assistant (CB, LC, DF, AF, XH, MK, MK, KK, AM, EM, WS, JHS, VS), pp. 252–255.
- CADE-1997-HutterK #λ-calculus
- A Colored Version of the Lambda-Calculus (DH, MK), pp. 291–305.
- CADE-1994-HuangKKMNRS #development #named #proving
- Omega-MKRP: A Proof Development Environment (XH, MK, MK, EM, DN, JR, JHS), pp. 788–792.
- CADE-1994-HuangKKMNRS94a #automation #deduction #named #tool support
- KEIM: A Toolkit for Automated Deduction (XH, MK, MK, EM, DN, JR, JHS), pp. 807–810.
- CADE-1994-JohannK #constant #order #unification #λ-calculus
- Unification in an Extensional Lambda Calculus with Ordered Function Sorts and Constant Overloading (PJ, MK), pp. 620–634.
- CADE-1994-KerberK #logic
- A Mechanization of Strong Kleene Logic for Partial Functions (MK, MK), pp. 371–385.
- ILPS-1993-KohlhaseP #unification #λ-calculus
- Unification in a λ-Calculus with Intersection Types (MK, FP), pp. 488–505.
- IJCAR-2018-MullerRK
- Theories as Types (DM0, FR, MK), pp. 575–590.