Abstract
This paper presents a method of deciding extended modal formulas that arise, in particular, when reasoning about transformations of relational structures and graphs. The method proceeds by first unwinding a structure that is an over-approximation of potential models, and then selecting effective models with the aid of a SAT solver.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Areces, C., Fontaine, P., Merz, S.: Modal satisfiability via SMT solving. In: De Nicola, R., Hennicker, R. (eds.) Software, Services, and Systems. LNCS, vol. 8950, pp. 30–45. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-15545-6_5
Baader, F., Lutz, C.: Description logic. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) The Handbook of Modal Logic, pp. 757–820. Elsevier (2006)
Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14
Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS (LNAI), vol. 5663, pp. 151–156. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02959-2_12
Brenas, J.H., Echahed, R., Strecker, M.: A hoare-like calculus using the SROIQ\(^{\sigma }\) logic on transformations of graphs. In: Diaz, J., Lanese, I., Sangiorgi, D. (eds.) TCS 2014. LNCS, vol. 8705, pp. 164–178. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44602-7_14
Giunchiglia, E., Tacchella, A., Giunchiglia, F.: SAT-based decision procedures for classical modal logics. J. Autom. Reason. 28(2), 143–171 (2002). https://doi.org/10.1023/A:1015071400913
Haarslev, V., Sebastiani, R., Vescovi, M.: Automated reasoning in \(\cal{ALCQ}\) via SMT. In: Bjørner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 283–298. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22438-6_22
Jackson, D.: Software Abstractions. MIT Press, Cambridge (2011)
Reynolds, A., Barbosa, H., Fontaine, P.: Revisiting enumerative instantiation. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 112–131. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89963-3_7
Sebastiani, R., Vescovi, M.: Automated reasoning in modal and description logics via SAT encoding: the case study of K (m)/ALC-satisfiability. J. Artif. Intell. Res. 35(1), 343 (2009)
Acknowledgements
Most of the work described here has been carried out while the author was at Inria Nancy during a research stay financially supported by Inria and hosted by the VeriDis team. I am grateful to Stephan Merz for inviting me, and to him and to Pascal Fontaine for discussions about and suggestions for improvement of this paper.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Strecker, M. (2018). Deciding Extended Modal Logics by Combining State Space Generation and SAT Solving. In: Fleuriot, J., Wang, D., Calmet, J. (eds) Artificial Intelligence and Symbolic Computation. AISC 2018. Lecture Notes in Computer Science(), vol 11110. Springer, Cham. https://doi.org/10.1007/978-3-319-99957-9_8
Download citation
DOI: https://doi.org/10.1007/978-3-319-99957-9_8
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-99956-2
Online ISBN: 978-3-319-99957-9
eBook Packages: Computer ScienceComputer Science (R0)