BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
Travelled to:
1 × Canada
1 × Denmark
1 × Germany
1 × Italy
1 × USA
2 × Australia
Collaborated with:
M.Kohlhase A.Steen G.Sutcliffe C.E.Brown F.Theiss F.Rabe L.C.Paulson A.Fietzke M.Wisniewski K.Kern J.H.Siekmann L.Cheikhrouhou A.Fiedler A.Meier E.Melis V.Sorge D.Fehrer X.Huang M.Kerber K.Konrad W.Schaarschmidt V.Brezhnev A.Franke H.Horacek M.Moschner I.Normann M.Pollet C.Ullrich C.Wirth J.Zimmer
Talks about:
higher (7) order (7) logic (4) theorem (3) prover (3) leo (3) extension (2) resolut (2) develop (2) omega (2)

Person: Christoph Benzmüller

DBLP DBLP: Benzm=uuml=ller:Christoph

Contributed to:

CADE 20092009
IJCAR 20082008
IJCAR 20062006
CADE 20022002
CADE 19991999
CADE 19981998
CADE 19971997
IJCAR 20162016
IJCAR 20182018

Wrote 11 papers:

CADE-2009-SutcliffeBBT #automation #development #higher-order #logic #proving #theorem proving
Progress in the Development of Automated Theorem Proving for Higher-Order Logic (GS, CB, CEB, FT), pp. 116–130.
IJCAR-2008-BenzmullerPTF #automation #higher-order #logic #named #proving #theorem proving
LEO-II — A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (CB, LCP, FT, AF), pp. 162–170.
IJCAR-2008-BenzmullerRS #higher-order #logic #named
THF0 — The Core of the TPTP Language for Higher-Order Logic (CB, FR, GS), pp. 491–506.
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-1999-Benzmuller #higher-order
Extensional Higher-Order Paramodulation and RUE-Resolution (CB), pp. 399–413.
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.
IJCAR-2016-WisniewskiSKB #effectiveness #normalisation
Effective Normalization Techniques for HOL (MW, AS, KK, CB), pp. 362–370.
IJCAR-2018-SteenB #higher-order #proving
The Higher-Order Prover Leo-III (AS, CB), pp. 108–116.

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.