\(\mathrm{K}_{\mathrm S}\mathrm{P}\) a resolution-based theorem prover for \({\mathsf{K}}_n\): architecture, refinements, strategies and experiments. (English) Zbl 1468.68304

Summary: In this paper we describe the implementation of \(\mathrm{K}_{\mathrm S}\mathrm{P}\), a resolution-based prover for the basic multimodal logic \({\mathsf{K}}_n\). The prover implements a resolution-based calculus for both local and global reasoning. The user can choose different normal forms, refinements of the basic resolution calculus, and strategies. We describe these options in detail and discuss their implications. We provide experiments comparing some of these options and comparing the prover with other provers for this logic.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
03B35 Mechanization of proofs and logical operations
03B45 Modal logic (including the logic of norms)
Full Text: DOI


[1] Areces, C., Gennari, R., Heguiabehere, J., de Rijke, M.: Tree-based heuristics in modal theorem proving. In: W. Horn (ed.) ECAI 2000, pp. 199-203. IOS Press, Amsterdam (2000)
[2] Areces, Carlos; Heguiabehere, Juan, HyLoRes 1.0: Direct Resolution for Hybrid Logics, Automated Deduction—CADE-18, 156-160 (2002), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1072.68560
[3] Balbiani, P., Demri, S.: Prefixed tableaux systems for modal logics with enriched languages. In: M.E. Pollack (ed.) IJCAI 1997, pp. 190-195. Morgan Kaufmann, Los Altos (1997)
[4] Balsiger, P.; Heuerding, A.; Schwendimann, S., A benchmark method for the propositional modal logics K, KT, S4, J. Automat. Reason., 24, 3, 297-317 (2000) · Zbl 0955.03013
[5] Basin, D.; Matthews, S.; Vigano, L., Labelled propositional modal logics: theory and practice, J. Logic Comput., 7, 6, 685-717 (1997) · Zbl 0902.03007
[6] Blackburn, P.; De Rijke, M.; Venema, Y., Modal Logic (2001), Cambridge: Cambridge University Press, Cambridge
[7] De La Tour, Tb, An optimality result for clause form translation, J. Symb. Comput., 14, 4, 283-301 (1992) · Zbl 0772.68079
[8] Fagin, R.; Halpern, Jy; Moses, Y.; Vardi, My, Reasoning About Knowledge (1995), Cambridge: MIT Press, Cambridge · Zbl 0839.68095
[9] Fisher, M.; Dixon, C.; Peim, M., Clausal temporal resolution, ACM Trans. Comput. Logic, 2, 1, 12-56 (2001) · Zbl 1365.03017
[10] Fitting, M., Prefixed tableaus and nested sequents, Ann. Pure Appl. Logic, 163, 3, 291-313 (2012) · Zbl 1241.03021
[11] Fitting, M.; Mendelsohn, Rl, First-Order Modal Logic (1998), Dordrecht: Kluwer, Dordrecht
[12] Flex: The fast lexical analyzer generator. http://github.com/westes/flex (2017). Accessed 6 Dec 2018
[13] GNU Bison: The yacc-compatible parser generator. http://www.gnu.org/software/bison/ (2017). Accessed 6 Dec 2018
[14] Goranko, V.; Passy, S., Using the universal modality: gains and questions, J. Logic Comput., 2, 1, 5-30 (1992) · Zbl 0774.03003
[15] Goré, Rajeev; Olesen, Kerry; Thomson, Jimmy, Implementing Tableau Calculi Using BDDs: BDDTab System Description, Automated Reasoning, 337-343 (2014), Cham: Springer International Publishing, Cham · Zbl 1423.68416
[16] Götzmann, D., Kaminski, M.: Spartacus: sources and benchmarks. Saarland University, Saarbrücken, Germany. http://www.ps.uni-saarland.de/spartacus/. Accessed 6 Dec 2018
[17] Götzmann, D.; Kaminski, M.; Smolka, G., Spartacus: a tableau prover for hybrid logic, Electron. Notes Theor. Comput. Sci., 262, 127-139 (2010)
[18] Hailpern, Bt, Verifying Concurrent Processes Using Temporal Logic (1982), Berlin: Springer, Berlin · Zbl 0476.68015
[19] Halpern, Jy, Using reasoning about knowledge to analyze distributed systems, Ann. Rev. Comput. Sci., 2, 37-68 (1987)
[20] Halpern, J.Y., Manna, Z., Moszkowski, B.: A hardware semantics based on temporal intervals. In: J. Díaz (ed.) ICALP 1983, LNCS, vol. 154, pp. 278-291. Springer, Berlin (1983) · Zbl 0534.68025
[21] Halpern, Jy; Moses, Y., A guide to completeness and complexity for modal logics of knowledge and belief, Artif. Intell., 54, 3, 319-379 (1992) · Zbl 0762.68029
[22] Hayes, Pj; Kowalski, Ra; Meltzer, B.; Michie, D., Semantic trees in automatic theorem proving, Machine Intelligence, 87-101 (1969), Amsterdam: Elsevier, Amsterdam · Zbl 0217.54001
[23] Horrocks, Ir; Hustadt, U.; Sattler, U.; Schmidt, R.; Blackburn, P.; Van Benthem, J.; Wolter, F., Computational modal logic, Handbook of Modal Logic, 181-245 (2006), Amsterdam: Elsevier, Amsterdam
[24] Hustadt, Ullrich; Schmidt, Renate A., MSPASS: Modal Reasoning by Translation and First-Order Resolution, Lecture Notes in Computer Science, 67-71 (2000), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0963.68522
[25] Jaeger, G., Balsiger, P., Heuerding, A., Schwendimann, S., Bianchi, M., Guggisberg, K., Janssen, G., Heinle, W., Achermann, F., Boroumand, A.D., Brambilla, P., Bucher, I., Zimmermann, H.: LWB: the logics workbench 1.1. University of Berne, Switzerland. http://home.inf.unibe.ch/ lwb/benchmarks/benchmarks.html. Accessed 6 Dec 2018
[26] Kaminski, M., Tebbi, T.: InKreSAT: sources and benchmarks. Saarland University, Germany. http://www.ps.uni-saarland.de/ kaminski/inkresat/. Accessed 6 Dec 2018
[27] Kaminski, Mark; Tebbi, Tobias, InKreSAT: Modal Reasoning via Incremental Reduction to SAT, Automated Deduction - CADE-24, 436-442 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1381.68272
[28] Kovács, Laura; Voronkov, Andrei, First-Order Theorem Proving and Vampire, Computer Aided Verification, 1-35 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[29] Lee, R.C.T.: A completeness theorem and computer program for finding theorems derivable from given axioms. Ph.D. thesis, University of California, Berkeley, USA (1967)
[30] Massacci, Fabio; Donini, Francesco M., Design and Results of TANCS-2000 Non-classical (Modal) Systems Comparison, Lecture Notes in Computer Science, 52-56 (2000), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0963.68518
[31] McCune, W.W.: OTTER 3.0 reference manual and guide. Technical report ANL-94/6, Argonne National Lab, Lemont, IL, USA (1994). http://www.osti.gov/servlets/purl/10129052-6WVVjK/native/. Accessed 6 Dec 2018
[32] Nalon, Cláudia; Dixon, Clare, Anti-prenexing and Prenexing for Modal Logics, Logics in Artificial Intelligence, 333-345 (2006), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1152.03320
[33] Nalon, C.; Dixon, C., Clausal resolution for normal modal logics, J. Algorithms, 62, 117-134 (2007) · Zbl 1131.03007
[34] Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare, A Modal-Layered Resolution Calculus for K, Lecture Notes in Computer Science, 185-200 (2015), Cham: Springer International Publishing, Cham · Zbl 1471.03017
[35] Nalon, Cláudia; Hustadt, Ullrich; Dixon, Clare, : A Resolution-Based Prover for Multimodal K, Automated Reasoning, 406-415 (2016), Cham: Springer International Publishing, Cham · Zbl 1475.68444
[36] Nalon, C., Hustadt, U., Dixon, C.: [inline-graphic not available: see fulltext] : sources and benchmarks. University of Brasília, Brazil (2018). http://www.cic.unb.br/ nalon/#software. Accessed 6 Dec 2018
[37] Nonnengart, A.; Weidenbach, C.; Robinson, A.; Voronkov, A., Computing small clause normal forms, Handbook of Automated Reasoning, 335-367 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0992.03018
[38] Olesen, K.: BDDTab: sources and benchmarks. Australian National University, Canberra, Australia. http://users.cecs.anu.edu.au/ rpg/BDDTab/. Accessed 6 Dec 2018
[39] Pan, G.; Sattler, U.; Vardi, My, BDD-based decision procedures for the modal logic K, J. Appl. Non Class. Logics, 16, 1-2, 169-208 (2006) · Zbl 1184.68466
[40] Patel-Schneider, Pf; Sebastiani, R., A new general method to generate random modal formulae for testing decision procedures, J. Artif. Intell. Res. (JAIR), 18, 351-389 (2003) · Zbl 1056.68136
[41] Plaisted, Da; Greenbaum, S., A structure-preserving clause form translation, J. Symb. Comput., 2, 3, 293-304 (1986) · Zbl 0636.68119
[42] Pratt, Vr, Application of modal logic to programming, Stud. Log., 39, 2-3, 257-274 (1980) · Zbl 0457.03013
[43] Rao, A.S., Georgeff, M.P.: Modeling rational agents within a BDI-architecture. In: R. Fikes, E. Sandewall (eds.) KR 1991, pp. 473-484. Morgan Kaufmann, Los Altos (1991) · Zbl 0765.68194
[44] Robinson, Ja, Automatic deduction with hyper-resolution, Int. J. Comput. Math., 1, 227-234 (1965) · Zbl 0158.26003
[45] Robinson, Ja, A machine-oriented logic based on the resolution principle, J. ACM, 12, 1, 23-41 (1965) · Zbl 0139.12303
[46] Schild, K.: A correspondence theory for terminological logics. In: J. Mylopoulos, R. Reiter (eds.) IJCAI 1991, pp. 466-471. Morgan Kaufmann, Los Altos (1991) · Zbl 0742.68059
[47] Schulz, S.; Bonacina, Mp; Stickel, Me, Simple and efficient clause subsumption with feature vector indexing, Automated Reasoning and Mathematics: Essays in Honour of William W. McCune, 45-67 (2013), Berlin: Springer, Berlin · Zbl 1383.68082
[48] Schuppan, Viktor; Darmawan, Luthfi, Evaluating LTL Satisfiability Solvers, Automated Technology for Verification and Analysis, 397-413 (2011), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[49] 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-389 (2009) · Zbl 1180.68257
[50] Spaan, E.: Complexity of modal logics. Ph.D. thesis, University of Amsterdam, The Netherlands (1993) · Zbl 0831.03005
[51] Tsarkov, D.: FaCT++: sources. https://github.com/ethz-asl/libfactplusplus. Accessed 6 Dec 2018
[52] Tsarkov, Dmitry; Horrocks, Ian, FaCT++ Description Logic Reasoner: System Description, Automated Reasoning, 292-297 (2006), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[53] Voronkov, A., Kovács, L., Reger, G., Suda, M., Kotelnikov, E., Robillard, S., Gleiss, B., Rawson, M., Bhayat, A., Riener, M.: Vampire. https://vprover.github.io/. Accessed 6 Dec 2018
[54] Waaler, A.; Robinson, Ja; Voronkov, A., Connections in nonclassical logics, Handbook of Automated Reasoning, 1487-1578 (2001), Amsterdam: Elsevier, Amsterdam · Zbl 0992.03020
[55] Wallen, La, Automated Deduction in Non-classical Logics (1990), Cambridge: MIT Press, Cambridge
[56] Wos, L.; Robinson, Ga; Carson, Df, Efficiency and completeness of the set of support strategy in theorem proving, J. ACM, 12, 536-541 (1965) · Zbl 0135.18401
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.