Home > Research > Publications & Outputs > Terminating Minimal Model Generation Procedures...

Research

Associated organisational unit

Links

Text available via DOI:

View graph of relations

Terminating Minimal Model Generation Procedures for Propositional Modal Logics

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Published

Standard

Terminating Minimal Model Generation Procedures for Propositional Modal Logics. / Papacchini, Fabio; Schmidt, Renate A.
Automated Reasoning - 7th International Joint Conference, IJCAR . Vol. 8562 Cham: Springer, 2014. p. 381-395.

Research output: Contribution in Book/Report/Proceedings - With ISBN/ISSN › Conference contribution/Paper › peer-review

Harvard

Papacchini, F & Schmidt, RA 2014, Terminating Minimal Model Generation Procedures for Propositional Modal Logics. in Automated Reasoning - 7th International Joint Conference, IJCAR . vol. 8562, Springer, Cham, pp. 381-395, International Joint Conference on Automated Reasoning, Vienna , Austria, 19/07/14. https://doi.org/10.1007/978-3-319-08587-6\_30

APA

Papacchini, F., & Schmidt, R. A. (2014). Terminating Minimal Model Generation Procedures for Propositional Modal Logics. In Automated Reasoning - 7th International Joint Conference, IJCAR (Vol. 8562, pp. 381-395). Springer. https://doi.org/10.1007/978-3-319-08587-6\_30

Vancouver

Papacchini F, Schmidt RA. Terminating Minimal Model Generation Procedures for Propositional Modal Logics. In Automated Reasoning - 7th International Joint Conference, IJCAR . Vol. 8562. Cham: Springer. 2014. p. 381-395 doi: 10.1007/978-3-319-08587-6\_30

Author

Papacchini, Fabio ; Schmidt, Renate A. / Terminating Minimal Model Generation Procedures for Propositional Modal Logics. Automated Reasoning - 7th International Joint Conference, IJCAR . Vol. 8562 Cham : Springer, 2014. pp. 381-395

Bibtex

@inproceedings{5101223b08564e55aa12394a7e78d8e9,
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.",
author = "Fabio Papacchini and Schmidt, {Renate A.}",
year = "2014",
month = jul,
day = "22",
doi = "10.1007/978-3-319-08587-6\_30",
language = "English",
isbn = "9783319085869",
volume = "8562",
pages = "381--395",
booktitle = "Automated Reasoning - 7th International Joint Conference, IJCAR",
publisher = "Springer",
note = "International Joint Conference on Automated Reasoning ; Conference date: 19-07-2014 Through 22-07-2014",
url = "https://link.springer.com/book/10.1007/978-3-319-08587-6",

}

RIS

TY - GEN

T1 - Terminating Minimal Model Generation Procedures for Propositional Modal Logics

AU - Papacchini, Fabio

AU - Schmidt, Renate A.

PY - 2014/7/22

Y1 - 2014/7/22

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.

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.

U2 - 10.1007/978-3-319-08587-6\_30

DO - 10.1007/978-3-319-08587-6\_30

M3 - Conference contribution/Paper

SN - 9783319085869

VL - 8562

SP - 381

EP - 395

BT - Automated Reasoning - 7th International Joint Conference, IJCAR

PB - Springer

CY - Cham

T2 - International Joint Conference on Automated Reasoning

Y2 - 19 July 2014 through 22 July 2014

ER -