Home > Research > Publications & Outputs > Terminating Minimal Model Generation Procedures...
View graph of relations

Terminating Minimal Model Generation Procedures for Propositional Modal Logics

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSNConference contribution/Paperpeer-review

Published
Publication date22/07/2014
Host publicationAutomated Reasoning - 7th International Joint Conference, IJCAR
Place of PublicationCham
PublisherSpringer
Pages381-395
Number of pages15
Volume8562
ISBN (electronic)9783319085876
ISBN (print)9783319085869
<mark>Original language</mark>English
EventInternational Joint Conference on Automated Reasoning - Vienna , Austria
Duration: 19/07/201422/07/2014
https://link.springer.com/book/10.1007/978-3-319-08587-6

Conference

ConferenceInternational Joint Conference on Automated Reasoning
Country/TerritoryAustria
CityVienna
Period19/07/1422/07/14
Internet address

Conference

ConferenceInternational Joint Conference on Automated Reasoning
Country/TerritoryAustria
CityVienna
Period19/07/1422/07/14
Internet address

Abstract

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, they are designed to have smaller search space and return fewer models. In order to make the models more effective for users, our minimal model criterion is aimed to be semantically meaningful, intuitive and contain a minimal amount of information. Depending on the logic, termination is ensured by a variation of equality blocking.