{"id":41,"date":"2015-08-27T11:07:52","date_gmt":"2015-08-27T11:07:52","guid":{"rendered":"http:\/\/dcis.inf.fu-berlin.de\/home\/?page_id=41"},"modified":"2021-06-03T19:25:21","modified_gmt":"2021-06-03T19:25:21","slug":"christoph-benzmueller-automated-reasoning","status":"publish","type":"page","link":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/workgroups\/christoph-benzmueller-automated-reasoning\/","title":{"rendered":"Benzm\u00fcller Group – Automated Reasoning"},"content":{"rendered":"

Christoph Benzm\u00fcller \u2013 Heisenberg Fellow of the German Research Foundation<\/h2>\n

Research topics: Logic (in CS, AI, Philosophy, Maths, Computational Linguistics),\u00a0Knowledge Representation and Reasoning, Automated and Interactive Theorem Proving, Formal Ontologies, Computational Metaphysics, Type theory<\/h5>\n\n\n\n
Christoph is well known for his automated higher-order theorem provers LEO-I and LEO-II. The latter system was developed in a project at Cambridge University, UK (2006-2007). Previously, Christoph has also been working at the boundry of computational logic, artificial intelligence, computational linguistics and computer-supported mathematics in several projects at Saarland University, the University of Birmingham, UK, and the University of Edinburgh, UK.\u00a0The latest research activities of Christoph include the automation of various quantified non-classical logics logics as natural fragments of classical higher-order logic, and the automation of challenge aspects, in particular, modal contexts, in ontology reasoning. In the latter research Christoph cooperated with Articulate Software, Angwin, CA, USA (2008-2011). Recently, Christoph received major international recognition for his work (with B. Woltzenlogel-Paleo) on the formalization and automation of Kurt G\u00f6del’s ontological argument for the existence of God on the computer.\n

\u00a0<\/p>\n

Christoph is trustee and vice-president of CADE (Conference on Automated Deduction), board member of AAR (Association of Automated Reasoning) and spokesman of the section Deduction Systems of the Gesellschaft f\u00fcr Informatik. He is editorial board member of the Journal of Applied Logic and the Logic Journal of the IGPL, and a permanent steering committee member of the User Interfaces for Theorem Provers workshop series. Moreover, he served as a trustee or steering committee member of several other conferences and he is an executive officer of The International Federation for Computational Logic (IFCoLog).<\/p>\n\n\n\n\n\n\n\n\n\n\n\n
Address<\/td>\nFreie Universit\u00e4t Berlin
Department of Mathematics and Computer Science
Arnimallee 7
D – 14195 Berlin<\/td>\n<\/tr>\n
Room<\/td>\n—<\/td>\n<\/tr>\n
Office hours<\/td>\n—<\/td>\n<\/tr>\n
Phone<\/td>\n+49 (0) 30 838 – 75102 \/ 52485<\/td>\n<\/tr>\n
Fax<\/td>\n+49 (0) 30 838 – 465301<\/td>\n<\/tr>\n
Email<\/td>\nc.benzmueller@fu-berlin.de<\/a><\/td>\n<\/tr>\n
Location<\/td>\nMaps and Directions<\/a><\/td>\n<\/tr>\n
Research<\/td>\nDetailed description of research interests<\/a><\/td>\n<\/tr>\n
Homepage<\/td>\nchristoph-benzmueller.de<\/a><\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n<\/td>\n\n
\"Christoph<\/a>

Christoph Benzm\u00fcller<\/p><\/div>\n<\/td>\n<\/tr>\n<\/tbody>\n<\/table>\n\n","protected":false},"excerpt":{"rendered":"

Christoph Benzm\u00fcller \u2013 Heisenberg Fellow of the German Research Foundation Research topics: Logic (in CS, AI, Philosophy, Maths, Computational Linguistics),\u00a0Knowledge Representation and Reasoning, Automated and Interactive Theorem Proving, Formal Ontologies, Computational Metaphysics, Type theory Christoph […]<\/p>\n","protected":false},"author":2,"featured_media":42,"parent":58,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"full-width-page.php","meta":[],"_links":{"self":[{"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/pages\/41"}],"collection":[{"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/comments?post=41"}],"version-history":[{"count":21,"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/pages\/41\/revisions"}],"predecessor-version":[{"id":394,"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/pages\/41\/revisions\/394"}],"up":[{"embeddable":true,"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/pages\/58"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/media\/42"}],"wp:attachment":[{"href":"https:\/\/dcmlr.inf.fu-berlin.de\/home\/wp-json\/wp\/v2\/media?parent=41"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}