Modal Tableau Systems with Blocking and Congruence Closure

Schmidt, R. A. and Waldmann, U. (2015)

In De Nivelle, H. (eds), Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX 2015). Lecture Notes in Computer Science, Vol. 9323, Springer, 38-53. BiBTeX, PDF (final version available via DOI link to Springer).

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.

Long version.

Renate A. Schmidt
Home | Publications | Tools | FM Group | School | Man Univ

Last modified: 21 Oct 15
Copyright © 2015 Renate A. Schmidt, School of Computer Science, Man Univ,