A General Tableau Method for Deciding Description Logics and Related Logics
Dr.-Ing. Renate A. Schmidt (University of Manchester)
NICTA LC SEMINARDATE: 2008-07-15
TIME: 16:00:00 - 17:00:00
LOCATION: NICTA - 7 London Circuit
CONTACT: JavaScript must be enabled to display this email address.
ABSTRACT:
In this talk we present a general method for proving termination of tableau-based procedures for modal-type logics and related first-order fragments. The central observation underlying the method is that most termination proofs for tableau decision procedures, can be seen to exploit techniques which look similar to standard filtration arguments in proofs of finite model property results. Our method provides a framework to turn given sound and complete tableau calculi into decision procedures by enhancing them with a flexible blocking mechanism. The framework can be applied to many description and modal logics, as well as first-order fragments. These include logics for which termination by tableau has so far been open. The framework is intended to be as generic and flexible as possible. As a consequence the techniques can be exploited in prover engineering platforms for contructing more general tableau decision procedures.
