Modal satisfiability via SMT solving. (English) Zbl 1453.03015
De Nicola, Rocco (ed.) et al., Software, services, and systems. Essays dedicated to Martin Wirsing on the occasion of his retirement from the chair of programming and software engineering, Munich, Germany, 2015. Essays. Cham: Springer. Lect. Notes Comput. Sci. 8950, 30-45 (2015).
Summary: Modal logics extend classical propositional logic, and they are robustly decidable. Whereas most existing decision procedures for modal logics are based on tableau constructions, we propose a framework for obtaining decision procedures by adding instantiation rules to standard SAT and SMT solvers. Soundness, completeness, and termination of the procedures can be proved in a uniform and elementary way for the basic modal logic and some extensions.
For the entire collection see [Zbl 1312.68005].
For the entire collection see [Zbl 1312.68005].
MSC:
| 03B45 | Modal logic (including the logic of norms) |
| 03B35 | Mechanization of proofs and logical operations |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Andréka, H., van Benthem, J., Németi, I.: Modal languages and bounded fragments of predicate logic. Journal of Philosophical Logic 27, 217–274 (1998) · Zbl 0919.03013 · doi:10.1023/A:1004275029985 |
| [2] | Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logics, pp. 821–868. Elsevier (2006) |
| [3] | Barrett, C., Sebastiani, R., Seshia, S.A., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, ch. 26, pp. 825–885. IOS Press (February 2009) |
| [4] | Bauer, F.L., Wirsing, M.: Elementare Aussagenlogik. Springer, Heidelberg (1991) · Zbl 0721.68001 · doi:10.1007/978-3-642-84263-4 |
| [5] | Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, vol. 53. Cambridge University Press, Cambridge (2001) · Zbl 0988.03006 · doi:10.1017/CBO9781107050884 |
| [6] | Bolander, T., Blackburn, P.: Termination for hybrid tableaus. Journal of Logic and Computation 17(3), 517–554 (2007) · Zbl 1140.03005 · doi:10.1093/logcom/exm014 |
| [7] | Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Berlin (1997) With an appendix by C. Allauzen, B. Durand · Zbl 0865.03004 · doi:10.1007/978-3-642-59207-2 |
| [8] | Chandra, A., Merlin, P.: Optimal implementation of conjunctive queries in relational databases. In: Proc. 9th ACM Symp. Theory of Computing, pp. 77–90 (1977) |
| [9] | Church, A.: A note on the Entscheidungsproblem. Journal of Symbolic Logic 1, 40–41 (1936) · JFM 62.1058.04 · doi:10.2307/2269326 |
| [10] | Ganzinger, H., Hustadt, U., Meyer, C., Schmidt, R.A.: A resolution-based decision procedure for extensions of K4. In: Zakharyaschev, M., Segerberg, K., de Rijke, M., Wansing, H. (eds.) Advances in Modal Logic, pp. 225–246. CSLI Publications (1998) · Zbl 0993.03017 |
| [11] | Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures: The case study of modal K(m). Information and Computation 162(1-2), 158–178 (2000) · Zbl 1033.03509 · doi:10.1006/inco.1999.2850 |
| [12] | Goranko, V., Passy, S.: Using the universal modality: Gains and questions. Journal of Logic and Computation 2(1), 5–30 (1992) · Zbl 0774.03003 · doi:10.1093/logcom/2.1.5 |
| [13] | Grädel, E.: Why are modal logics so robustly decidable? Bulletin EATCS 68, 90–103 (1999) · Zbl 0935.03029 |
| [14] | Grädel, E., Kolaitis, P., Vardi, M.: On the decision problem for two-variable first-order logic. Bulletin of Symbolc Logic 3, 53–69 (1997) · Zbl 0873.03009 · doi:10.2307/421196 |
| [15] | Grädel, E., Otto, M., Rosen, E.: Two-variable logic with counting is decidable. In: Proc. 12th Ann. IEEE Symp. Logic in Computer Science (LICS 1997), pp. 306–317. IEEE Comp. Soc. (1997) · doi:10.1109/LICS.1997.614957 |
| [16] | Hustadt, U., de Nivelle, H., Schmidt, R.A.: Resolution-based methods for modal logics. Logic Journal of the IGPL 8(3), 265–292 (2000) · Zbl 0947.03014 · doi:10.1093/jigpal/8.3.265 |
| [17] | Löwenheim, L.: Über Möglichkeiten im Relativkalkül. Mathematische Annalen 76, 447–470 (1915) · JFM 45.0108.01 · doi:10.1007/BF01458217 |
| [18] | Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937–977 (2006) · Zbl 1326.68164 · doi:10.1145/1217856.1217859 |
| [19] | Ohlbach, H.J., Schmidt, R.A.: Functional translation and second-order frame properties of modal logics. Journal of Logic and Computation 7(5), 581–603 (1997) · Zbl 0976.03019 · doi:10.1093/logcom/7.5.581 |
| [20] | Pacholsky, L., Szwast, W., Tendera, L.: Complexity of two-variable logic with counting. In: Proc. 12th Ann. IEEE Symp. Logic in Computer Science (LICS 1997), pp. 318–327 (1997) · doi:10.1109/LICS.1997.614958 |
| [21] | Schmidt, R.A., Hustadt, U.: First-order resolution methods for modal logics. In: Voronkov, A., Weidenbach, C. (eds.) Programming Logics. LNCS, vol. 7797, pp. 345–391. Springer, Heidelberg (2013) · Zbl 1383.03031 · doi:10.1007/978-3-642-37651-1_15 |
| [22] | Schmidt, R.A., Tishkovsky, D.: Using tableau to decide description logics with full role negation and identity. ACM Trans. Comput. Log. 15(1) (2014) · Zbl 1287.03031 · doi:10.1145/2559947 |
| [23] | Scott, D.: A decision method for validity of sentences in two variables. Journal of Symbolic Logic 27(377), 74 (1962) |
| [24] | Sebastiani, R., Tacchella, A.: SAT techniques for modal and description logics. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 781–824. IOS Press (2009) |
| [25] | Turing, A.: On computable numbers, with an application to the ’Entscheidungsproblem’. Proc. London Mathematical Society 2nd. series 42, 230–265 (1937) · Zbl 0016.09701 · doi:10.1112/plms/s2-42.1.230 |
| [26] | Vardi, M.: Why is modal logic so robustly decidable? In: DIMACS Ser. Disc. Math. Theoret. Comp. Sci., vol. 31, pp. 149–184. AMS (1997) · Zbl 0881.03012 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
