Developing Modal Tableaux and Resolution Methods via First-Order Resolution

Schmidt, R. A. (2006)

In Governatori, G. and Hodkinson, I. and Venema, Y. (eds), Advances in Modal Logic, Volume 6. College Publications, London, 1-26. Invited paper. BiBTeX, PostScript.

This paper explores the development of calculi using different proof methods for propositional dynamic modal logics. Dynamic modal logics are PDL-like extended modal logics which are closely related to description logics. We show how tableau systems, modal resolution systems and Rasiowa-Sikorski systems, which are dual tableau systems, can be developed and studied by using standard principles and methods of first-order theorem proving. We translate modal logic reasoning problems to first-order clausal form and then use a suitable refinement of resolution to construct and mimic derivations using the desired proof method. The inference rules of the calculus can then be read off from the clausal form used.

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

Last modified: 04 Oct 06
Copyright © 2005 Renate A. Schmidt, School of Computer Science, Man Univ,