Tutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL

Christoph Benzmüller, Alexander Steen, Max Wisniewski— 2016

Non-classical logics (such as modal logics, description logics, conditional logics, multi-valued logics, hybrid logics, etc.) have many applications in artificial intelligence. In this tutorial, we will demonstrate a generic approach to automate propositional and quantified variants of non-classical logics using theorem proving systems for classical higher-order logic. Our particular focus will be on quantified multimodal logics. We will present and discuss a semantical embedding of quantified multimodal logics into classical higher-order logic, which enables the encoding and automated analysis of non-trivial modal logic problems in the Isabelle/HOL proof assistant. Additionally, TPTP compliant automated theorem proving systems can be called from within Isabelle’s Sledgehammer tool for automating reasoning tasks. In the tutorial, we will apply this approach to exemplarily solve a prominent puzzle from the AI literature: the well-known wise men.

TitelTutorial on Reasoning in Expressive Non-Classical Logics with Isabelle/HOL
VerfasserChristoph Benzmüller, Alexander Steen, Max Wisniewski
KennungISSN: 2398-7340
Erschienen inProceedings of the GCAI 2016. 2nd Global Conference on Artificial Intelligence, EPiC Series in computing, vol. 41, 2016.
Größe oder Längepp. 1-10