Links und Funktionen
Sprachumschaltung

Navigationspfad
Sie sind hier: Startseite / Lehre / SS 2018 / Oberseminar / Christoph Benzmüller: Experiments in Universal Logical Reasoning — How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic?


Inhaltsbereich

Christoph Benzmüller: Experiments in Universal Logical Reasoning — How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic?

Oberseminar, Freitag, 25. Mai 2018, 14 Uhr c.t.
Wann 14:15 15:45 25.05.2018
von bis
Wo Raum L109, Oettingenstr. 67
Termin übernehmen vCal
iCal
Speaker: Christoph Benzmüller

Titel: Experiments in Universal Logical Reasoning — How to utilise ATPs and SMT solvers for the exploration of axiom systems for category theory in free logic?

Abstract: Classical higher-order logic, when utilized as a meta-logic in which various other (classical and non-classical) logics can be shallowly embedded, is suitable as a foundation for the development of a universal logical reasoning engine. Such an engine may be employed, as already envisioned by Leibniz, to support the rigorous formalisation and deep logical analysis of rational arguments on the computer.  

In my talk I will exemplarily demonstrate how this approach can be utilised to implement "free logic" within the proof assistant Isabelle/HOL. SMT solvers and ATPs, which are integrated with Isabelle/HOL, can be then be used in this framework to (indirectly) automate free logic reasoning. 

Free logic has many interesting applications, e.g. in natural language processing and as a logic of fiction. In mathematics, free logics are particularly suited in application domains, such as axiomatic category theory, where an adequate and elegant treatment of partiality and undefinedness is required. 

In my talk I will summarise the results of an experiment with the above free logic reasoner, in which a series of mutually equivalent axiom systems for category theory has been systematically explored. As a side-effect of this work some (minor) issue in a prominent category theory textbook has been revealed.

The purpose of this work is not to claim any novel results in category theory, but to demonstrate an elegant way to automate reasoning in free logic, and to present illustrative experiments, which were (indirectly) supported by SMT solvers, ATPs and the model finder Nitpick.

(This is joint work with Dana Scott.)

Bio: Christoph Benzmüller is affiliated as Privatdozent for Computer Science and Mathematics with Freie Universität Berlin and Saarland University, Saarbrücken. At present, he is visiting University of Luxemburg. Previous research stations of Christoph include Stanford University, USA (visiting scholar), Articulate Software, USA (senior researcher), Intl. University of Germany, Bruchsal (full professor), University of Cambridge, UK (senior researcher), Saarland University (associate professor), University of Birmingham, UK and the University of Edinburgh, UK (postdoc).

Christoph received his PhD (1999) and his Habilitation (2007) in computer science from Saarland University. His PhD was partly conducted at Carnegie Mellon University, USA. In 2012, Christoph had been awarded with a Heisenberg Research Fellowship of the German National Research Foundation (DFG).

Christoph is an expert in higher-order automated and interactive theorem proving, which he utilises as a basis for an approach towards universal logic reasoning. His broader interests concern all aspects of knowledge representation and reasoning. Moreover, Christoph is well known for his interdisciplinary applications. Most recently, for example, he has pioneered, together with colleagues, the area of computational metaphysics.

Artikelaktionen


Funktionsleiste