Terminating minimal model generation procedures for propositional modal logics

Fabio Papacchini; Renate A. Schmidt

doi:10.1007/978-3-319-08587-6-30

Terminating minimal model generation procedures for propositional modal logics

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

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. © 2014 Springer International Publishing Switzerland.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)\|Lect. Notes Comput. Sci.
Publisher	Springer Nature
Pages	381-395
Number of pages	14
Volume	8562
ISBN (Print)	9783319085869
DOIs	https://doi.org/10.1007/978-3-319-08587-6-30
Publication status	Published - 2014
Event	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 - Vienna Duration: 1 Jul 2014 → … http://springerlink.com/content/0302-9743/copyright/2005/http://dx.doi.org/10.1007/978-3-319-08587-6_30

Conference

Conference	7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014
City	Vienna
Period	1/07/14 → …
Internet address	http://springerlink.com/content/0302-9743/copyright/2005/http://dx.doi.org/10.1007/978-3-319-08587-6_30

Access to Document

10.1007/978-3-319-08587-6-30

Cite this

@inproceedings{1b22e6f41e06441ba9649716a9fcd59e,

title = "Terminating minimal model generation procedures for propositional modal logics",

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. {\textcopyright} 2014 Springer International Publishing Switzerland.",

author = "Fabio Papacchini and Schmidt, {Renate A.}",

year = "2014",

doi = "10.1007/978-3-319-08587-6-30",

language = "English",

isbn = "9783319085869",

volume = "8562",

pages = "381--395",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.",

publisher = "Springer Nature",

address = "United States",

note = "7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014 ; Conference date: 01-07-2014",

url = "http://springerlink.com/content/0302-9743/copyright/2005/http://dx.doi.org/10.1007/978-3-319-08587-6_30",

}

Papacchini, F & Schmidt, RA 2014, Terminating minimal model generation procedures for propositional modal logics. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. vol. 8562, Springer Nature, pp. 381-395, 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, 1/07/14. https://doi.org/10.1007/978-3-319-08587-6-30

Terminating minimal model generation procedures for propositional modal logics. / Papacchini, Fabio; Schmidt, Renate A.
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.. Vol. 8562 Springer Nature, 2014. p. 381-395.

Research output: Chapter in Book/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Terminating minimal model generation procedures for propositional modal logics

AU - Papacchini, Fabio

AU - Schmidt, Renate A.

PY - 2014

Y1 - 2014

N2 - 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. © 2014 Springer International Publishing Switzerland.

AB - 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. © 2014 Springer International Publishing Switzerland.

U2 - 10.1007/978-3-319-08587-6-30

DO - 10.1007/978-3-319-08587-6-30

M3 - Conference contribution

SN - 9783319085869

VL - 8562

SP - 381

EP - 395

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)|Lect. Notes Comput. Sci.

PB - Springer Nature

T2 - 7th International Joint Conference on Automated Reasoning, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014

Y2 - 1 July 2014

ER -

Terminating minimal model generation procedures for propositional modal logics

Abstract

Conference

Access to Document

Other files and links

Fingerprint

Cite this