Seminarraum Gödel, Institutsgebäude (Favoritenstr. 9-11) - EG, Zugang vom Innenhof

Expressive non-classical logics such as quantified modal logics or quantified conditional logics have many potential applications.

In this talk I address the question whether expressive non-classical logics, either individually or flexibly combined, can be mechanized and automated in a generic reasoning framework. This question is relevant beyond the boundaries of computer science and artificial intelligence.

I will outline a solution based on classical higher order logic (Church’s type theory). I will show that many expressive non-classical logics are just natural fragments of classical higher order logic and that also flexible combinations of these logic fragments can easily be modeled in it. A particular focus of the talk will be on quantified modal logics and their combinations; quantified conditional logics will also be addressed.

Employing the above approach off-the-shelf higher order automated theorem provers, like my own LEO-II system, and higher order model finders can be directly applied for reasoning within non-classical logics and their combinations. Interestingly, even automated verification and exploration of meta-level properties of logics and logic combinations is now feasible.