T1: Automated Theorem Proving in the TPTP World (Geoff Sutcliffe, University of Miami)
13:30--15:30, Thursday, September 29th, Seminarroom SR006, Takustrasse 9, Institut für Informatik, FU Berlin, see the map
ABSTRACT: The TPTP World is a well known and established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) systems for classical logics. The data, standards, and services provided by the TPTP World have made it increasingly easy to build, test, and apply ATP technology. This tutorial reviews the core features of the TPTP World, describes key service components of the TPTP World and how to use them, presents some successful applications, and gives an overview of planned developments.
T2: Interactive and Automated Theorem Proving for Non-Classical Logics (Christoph Benzmüller, Alexander Steen and Max Wisniewski, FU Berlin)
16:00--18:00, Thursday, September 29th, Seminarroom SR006, Takustrasse 9, Institut für Informatik, FU Berlin, see the map
ABSTRACT: Non-classical logics (such as modal logic, description logic, conditional logic, multi-valued logic, nominal logic, etc.) have many applications in AI. In this tutorial we will demonstrate a generic approach to automate propositional and quantified variants of non-classical logics in theorem proving systems for classical higher-order logic (HOL). Our particular focus will be on quantified multi-modal logic (QMMF). We will present and discuss the embedding of QMMF in the Isabelle/HOL proof assistant. Utilising this embedding, TPTP compliant automated theorem proving systems can be called from within Isabelle/HOL to solve reasoning tasks formulated in QMMF. In the tutorial we will apply the approach to exemplarily solve a prominent puzzle from the AI literature: the well known muddy forehead puzzle (resp. wise men puzzle).