BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
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.