Terminating Minimal Model Generation Procedures for Propositional Modal Logics.

Papacchini, F. and Schmidt, R. A. (2014)

In S. Demri, D. Kapur, C. Weidenbach (eds), Automated Reasoning (IJCAR 2014). Lecture Notes in Artificial Intelligence, Vol. 8562, Springer, 381-395. BiBTeX, PDF (final version available via DOI link to Springer).

Model generation and minimal model generation are useful for tasks such as model checking and for debugging of logical specifications. This paper presents terminating procedures for the generation of models minimal modulo subset-simulation for the modal logic K and all combinations of extensions with the axioms T, B, D, 4 and 5. Our procedures are minimal model sound and complete. Compared with other minimal model generation procedures, our procedures benefit from smaller search spaces and fewer models are returned. To make the models most effective for users, our minimal model criterion is designed to be semantically meaningful, intuitive and contain minimal amount of information. Depending on the logic, termination is ensured by a variation of equality blocking.


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

Last modified: 01 Dec 14
Copyright © 2014 Renate A. Schmidt, School of Computer Science, Man Univ, schmidt@cs.man.ac.uk