Modal tableau systems with blocking and congruence closure

R.A. Schmidt, Uwe Waldmann

Research output: Chapter in Book/Conference proceedingConference contributionpeer-review

Abstract

Our interest in this paper are semantic tableau approaches closely related to bottom-up model generation methods. Using equality-based blocking techniques these can be used to decide logics representable in first-order logic that have the finite model property. Many common modal and description logics have these properties and can therefore be decided in this way. This paper integrates congruence closure, which is probably the most powerful and efficient way to realise reasoning with ground equations, into a modal tableau system with equality-based blocking. The system is described for an extension of modal logic K characterised by frames in which the accessibility relation is transitive and every world has a distinct immediate predecessor. We show the system is sound and complete, and discuss how various forms of blocking such as ancestor blocking can be realised in this setting. Though the investigation is focussed on a particular modal logic, the modal logic was chosen to show the most salient ideas and techniques for the results to be generalised to other tableau calculi and other logics.
Original languageEnglish
Title of host publicationAutomated reasoning with analytic tableaux and related methods
Subtitle of host publication24th international conference, TABLEAUX 2015, Wroclaw, Poland, September 21-24, 2015, proceedings
EditorsHans De Nivelle
Place of PublicationCham, Switzerland
PublisherSpringer Nature
Pages38-53
Number of pages19
Volume9323
ISBN (Electronic) 9783319243122
ISBN (Print)9783319243115
DOIs
Publication statusPublished - 2015
EventTABLEAUX: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods: 24th International Conference - Wroclaw, Poland
Duration: 21 Sept 201524 Sept 2015

Publication series

NameLecture notes in artificial intelligence
PublisherSpringer
Number9323

Conference

ConferenceTABLEAUX: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods
Abbreviated titleTABLEAUX 2015
Country/TerritoryPoland
CityWroclaw
Period21/09/1524/09/15

Fingerprint

Dive into the research topics of 'Modal tableau systems with blocking and congruence closure'. Together they form a unique fingerprint.

Cite this