research-article

Open access

Modal Resolution: Proofs, Layers, and Refinements

Authors:

Cláudia Nalon,

Ullrich HustadtAuthors Info & Claims

ACM Transactions on Computational Logic (TOCL), Volume 20, Issue 4

Article No.: 23, Pages 1 - 38

https://doi.org/10.1145/3331448

Published: 13 August 2019 Publication History

All formats PDF

Abstract

Resolution-based provers for multimodal normal logics require pruning of the search space for a proof to ameliorate the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution calculus for the basic multimodal logic, which divides the clause set according to the modal level at which clauses occur to reduce the number of possible inferences. We show that the calculus is complete for the logics being considered. We also show that the calculus can be combined with other strategies. In particular, we discuss the completeness of combining modal layering with negative and ordered resolution and provide experimental results comparing the different refinements.

References

[1]

Hajnal Andréka, Johan van Benthem, and Istvan Németi. 1998. Modal logics and bounded fragments of predicate logic. J. Philos. Logic 27, 3 (1998), 217--274.

[2]

Carlos Areces, Rosella Gennari, Juan Heguiabehere, and Maarten de Rijke. 2000. Tree-based heuristics in modal theorem proving. In Proceedings of the 14th European Conference on Artificial Intelligence (ECAI’00). IOS Press, 199--203.

Digital Library

[3]

Carlos Areces and Daniel Gorín. 2011. Resolution with order and selection for hybrid logics. J. Auto. Reason. 46, 1 (2011), 1--42.

Digital Library

[4]

Carlos Areces and Juan Heguiabehere. 2002. HyLoRes 1.0: Direct resolution for hybrid logics. In Proceedings of the 18th International Conference on Automated Deduction (CADE'18). Lecture Notes in Computer Science, vol. 2392. 156--160.

Digital Library

[5]

Carlos Areces, Hans de Nivelle, and Maarten de Rijke. 1999. Prefixed resolution: A resolution method for modal and description logics. In Proceedings of the 16th International Conference on Automated Deduction (CADE’99) (Lecture Notes in Artificial Intelligence), vol. 1632. Springer, 187--201.

Digital Library

[6]

Franz Baader, Diego Calvanese, Deborah L. McGuinness, Daniele Nardi, and Peter F. Patel-Schneider. 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press.

Digital Library

[7]

Matthias Baaz, Uwe Egly, and Alexander Leitsch. 2001. Normal form transformations. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.), vol. I. Elsevier and MIT Press, 273--333.

[8]

Matthias Baaz and Christian G. Fermüller. 1992. Resolution for many-valued logics. In Proceedings of the International Conference on Logic Programming and Automated Reasoning (LPAR’92) (Lecture Notes in Computer Science), Andre Voronkov (Ed.), vol. 624. Springer, 107--118.

Digital Library

[9]

Matthias Baaz, Christian G. Fermüller, and Gernot Salzer. 2001. Automated deduction for many-valued logics. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.), vol. II. Elsevier and MIT Press, chap. 20, 1355--1402.

Digital Library

[10]

Leo Bachmair and Harald Ganzinger. 1990. On restrictions of ordered paramodulation with simplification. In Proceedings of the 10th International Conference on Automated Deduction (CADE’90) (Lecture Notes in Computer Science), vol. 449. Springer, 427--441.

Digital Library

[11]

Philippe Balbiani and Stéphane Demri. 1997. Prefixed tableaux systems for modal logics with enriched languages. In Proceedings of the 15th International Joint Conference on Artificiall Intelligence (JCAI’97). Morgan Kaufmann, 190--195.

Digital Library

[12]

Peter Balsiger, Alain Heuerding, and Stefan Schwendimann. 2000. A benchmark method for the propositional modal logics K, KT, S4. J. Auto. Reason. 24, 3 (2000), 297--317.

Digital Library

[13]

David Basin, Sean Matthews, and Luca Vigano. 1997. Labelled propositional modal logics: Theory and practice. J. Logic Comput. 7, 6 (1997), 685--717.

[14]

Patrick Blackburn, Maarten de Rijke, and Yde Venema. 2001. Modal Logic. Cambridge University Press.

[15]

Torben Braüner. 2014. Hybrid logic. In Handbook of Philosophical Logic, vol. 17. Dov M. Gabbay and Franz Guenthner (Eds.). Springer, 1--77.

[16]

Luis Fariñas del Cerro and Andreas Herzig. 1988. Linear modal deductions. In Proceedings of the 9th International Conference on Automated Deduction (CADE’88) (Lecture Notes in Computer Science), vol. 310. Springer, 487--499.

Digital Library

[17]

Melvin Fitting. 2012. Prefixed tableaus and nested sequents. Ann. Pure Appl. Logic 163, 3 (2012), 291--313.

[18]

Melvin Fitting and Richard L. Mendelsohn. 1998. First-Order Modal Logic. Kluwer.

[19]

Valentin Goranko and Solomon Passy. 1992. Using the universal modality: Gains and questions. J. Logic Comput. 2, 1 (1992), 5--30.

[20]

Rajeev Goré, Kerry Olesen, and Jimmy Thomson. 2014. Implementing tableau calculi using BDDs: BDDTab system description. In Proceedings of the 7th International Joint Conference on Automated Deduction (IJCAR’14) (Lecture Notes in Computer Science), vol. 8562. Springer, 337--343.

[21]

Daniel Götzmann, Mark Kaminski, and Gert Smolka. 2010. Spartacus: A tableau prover for hybrid logic. Electron. Notes Theoret. Comput. Sci. 262 (2010), 127--139.

Digital Library

[22]

Reiner Hähnle. 1993. Automated Deduction in Multiple-Valued Logics. Oxford University Press.

Digital Library

[23]

Brent T. Hailpern. 1982. Verifying Concurrent Processes Using Temporal Logic. Lecture Notes in Computer Science, vol. 129. Springer.

Digital Library

[24]

Joseph Y. Halpern. 1987. Using reasoning about knowledge to analyze distributed systems. Annu. Rev. Comput. Sci. 2 (1987), 37--68.

[25]

Joseph Y. Halpern, Zohar Manna, and Ben Moszkowski. 1983. A hardware semantics based on temporal intervals. In Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP’83). Lecture Notes in Computer Science, vol. 154, 278--291.

Digital Library

[26]

Joseph Y. Halpern and Yoram Moses. 1992. A guide to completeness and complexity for modal logics of knowledge and belief. Artific. Intell. 54, 3 (Apr. 1992), 319--379.

Digital Library

[27]

Patrick J. Hayes and Robert A. Kowalski. 1969. Semantic trees in automatic theorem proving. In Proceedings of the 4th Annual Machine Intelligence Workshop. Elsevier, 87--101.

[28]

Ian Horrocks, Ullrich Hustadt, Ulrike Sattler, and Renate A. Schmidt. 2006. Computational modal logic. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Elsevier, 181--245.

[29]

Ullrich Hustadt and Boris Konev. 2004. TRP++: A temporal resolution prover. In Collegium Logicum. Kurt Gödel Society, 65--79.

[30]

Mark Kaminski and Tobias Tebbi. 2013. InKreSAT: Modal reasoning via incremental reduction to SAT. In Proceedings of the 24th International Conference on Automated Deduction (CADE’13) (Lecture Notes in Artificial Intelligence), vol. 7898. Springer, 436--442.

Digital Library

[31]

Laura Kovács and Andrei Voronkov. 2013. First-order theorem proving and vampire. In Proceedings of the 25th International Conference on Computer Aided Verification (CAV’13) (Lecture Notes in Computer Science), vol. 8044. Springer, 1--35.

[32]

Richard E. Ladner. 1977. The computational complexity of provability in systems of modal propositional logic. SIAM J. Comput. 6, 3 (1977), 467--480.

Digital Library

[33]

Richard C. T. Lee. 1967. A Completeness Theorem and Computer Program for Finding Theorems Derivable from Given Axioms. Ph.D. Dissertation. Berkeley.

Digital Library

[34]

Maarten Marx. 2006. Complexity of modal logic. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Frank Wolter (Eds.). Elsevier, New York, 139--179.

[35]

Maarten Marx and Yde Venema. 2007. Local variations on a loose theme: Modal logic and decidability. In Finite Model Theory and Its Applications. Springer, 371--429.

[36]

Fabio Massacci and Francesco M. Donini. 2000. Design and results of TANCS-2000 non-classical (modal) systems comparison. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’00) (Lecture Notes in Computer Science), vol. 1847. Springer, 52--56.

Digital Library

[37]

William W. McCune. 2007. OTTER 3.0 reference manual and guide.

[38]

Eliana Minicozzi and Raymond Reiter. 1972. A note on linear resolution strategies in consequence-finding. Artific. Intell. 3, 1--3 (1972), 175--180.

Digital Library

[39]

Cláudia Nalon and Clare Dixon. 2007. Clausal resolution for normal modal logics. J. Algor. 62 (2007), 117--134. Issue 3-4.

Digital Library

[40]

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon. 2015. A modal-layered resolution calculus for K. In Proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX’15) (Lecture Notes in Computer Science), vol. 9323. Springer, 185--200.

Digital Library

[41]

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon. 2016. : K<sub>S</sub>P A resolution-based prover for multimodal K. In Proceedings of the 8th International Joint Conference on Automated Reasoning (IJCAR’16) (Lecture Notes in Computer Science), vol. 9706. Springer, 406--415.

Digital Library

[42]

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon. 2016. K<sub>S</sub>P : Sources and benchmarks. Retrieved from http://www.cic.unb.br/nalon/#software.

[43]

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon. 2017. K<sub>S</sub>P : A resolution-based prover for multimodal K, abridged report. In Proceedings of the 26th International Joint Conference on Artificial Intelligence (IJCAI’17). 4919--4923.

Digital Library

[44]

Cláudia Nalon, Ullrich Hustadt, and Clare Dixon. 2018. K<sub>S</sub>P a resolution-based theorem prover for K<sub>n</sub>: Architecture, refinements, strategies and experiments. J. Auto. Reason. To appear.

[45]

Andreas Nonnengart and Christoph Weidenbach. 2001. Computing small clause normal forms. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.), vol. 1. Elsevier and MIT Press, 335--367.

[46]

Hans Jürgen Ohlbach. 1988. A resolution calculus for modal logics. In Proceedings of the 9th International Conference on Automated Deduction (CADE’88) (Lecture Notes in Computer Science), vol. 310. Springer, 500--516.

Digital Library

[47]

Hans Jürgen Ohlbach. 1991. Semantics-based translation methods for modal logics. J. Logic Comput. 1, 5 (1991), 691--746.

[48]

Hans Jürgen Ohlbach and Renate A. Schmidt. 1997. Functional translation and second-order frame properties of modal logics. J. Logic Comput. 7, 5 (Oct. 1997), 581--603.

[49]

Guoqiang Pan and Moshe Y. Vardi. 2003. Optimizing a BDD-based modal solver. In Proceedings of the 19th International Conference on Automated Deduction (CADE’03) (Lecture Notes in Computer Science), vol. 2741. Springer, 75--89.

[50]

Peter F. Patel-Schneider and Roberto Sebastiani. 2003. A new general method to generate random modal formulae for testing decision procedures. J. Artific. Intell. Res. 18 (2003), 351--389.

Digital Library

[51]

David A. Plaisted and Steven A. Greenbaum. 1986. A structure-preserving clause form translation. J. Logic Comput. 2 (1986), 293--304.

Digital Library

[52]

Vaughan R. Pratt. 1980. Application of modal logic to programming. Studia Logica 39, 2/3 (1980), 257--274.

[53]

Anand S. Rao and Michael P. Georgeff. 1991. Modeling rational agents within a BDI-architecture. In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning (KR8R’91). Morgan-Kaufmann, 473--484.

Digital Library

[54]

John Alan Robinson. 1965. Automatic deduction with hyper-resolution. Int. J. Comput. Math. 1 (1965), 227--234.

[55]

John Alan Robinson. 1965. A machine--oriented logic based on the resolution principle. J. Assoc. Comput. Mach. 12, 1 (Jan. 1965), 23--41.

Digital Library

[56]

Klaus Schild. 1991. A correspondence theory for terminological logics. In Proceedings of the 12th International Joint Conference on Artificial Intelligence (IJCAI’91). Morgan Kaufmann, 466--471.

Digital Library

[57]

Renate A. Schmidt. 1999. Decidability by resolution for propositional modal logics. J. Auto. Reason. 22, 4 (1999), 379--396.

Digital Library

[58]

Stephan Schulz. 2013. The E Theorem Prover. Retrieved from http://wwwlehre.dhbw-stuttgart.de/ sschulz/E/E.html.

[59]

Stephan Schulz. 2013. Simple and efficient clause subsumption with feature vector indexing. In Automated Reasoning and Mathematics—Essays in Memory of William W. McCune (Lecture Notes in Computer Science), Maria Paola Bonacina and Mark E. Stickel (Eds.), vol. 7788. Springer, 45--67.

Digital Library

[60]

Frantisek Simancik, Boris Motik, and Ian Horrocks. 2014. Consequence-based and fixed-parameter tractable reasoning in description logics. Artific. Intell. 209 (2014), 29--77.

Digital Library

[61]

James R. Slagle. 1967. Automatic theorem proving with renamable and semantic resolution. J. ACM 14, 4 (Oct. 1967), 687--697.

Digital Library

[62]

James R. Slagle, C. L. Chang, and Richard C. T. Lee. 1969. Completeness theorems for semantic resolution in consequence-finding. In Proceedings of the 1st International Joint Conference on Artificial Intelligence (IJCAI’69). William Kaufmann, 281--286.

Digital Library

[63]

Edith Spaan. 1993. Complexity of Modal Logics. Ph.D. Dissertation. University of Amsterdam.

[64]

The SPASS Team. 2010. Automation of Logic: SPASS. Retrieved from http://www.spass-prover.org/.

[65]

Dmitry Tsarkov and Ian Horrocks. 2006. FaCT++ description logic reasoner: System description. In Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR’06) (Lecture Notes in Computer Science), vol. 4130. Springer, 292--297.

Digital Library

[66]

Andrei Voronkov. 2013. Vampire. Retrieved from http://www.vprover.org/index.cgi.

[67]

Arild Waaler. 2001. Connections in nonclassical logics. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Elsevier and MIT Press, 1487--1578.

Digital Library

[68]

Lincoln A. Wallen. 1990. Automated Deduction in Non-Classical Logics. MIT Press.

Digital Library

[69]

Larry Wos, George A. Robinson, and Daniel Carson. 1965. Efficiency and completeness of the set of support strategy in theorem proving. J. Assoc. Comput. Mach. 12 (1965), 536--541.

Digital Library

Cited By

Hustadt UPapacchini FNalon CDixon C(2024)Model Construction for Modal ClausesAutomated Reasoning10.1007/978-3-031-63501-4_1(3-23)Online publication date: 2-Jul-2024
https://doi.org/10.1007/978-3-031-63501-4_1
Pattinson DOlivetti NNalon C(2023)Resolution Calculi for Non-normal Modal LogicsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_18(322-341)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_18
Nalon CHustadt UPapacchini FDixon C(2023)Buy One Get 14 Free: Evaluating Local Reductions for Modal LogicAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_22(382-400)Online publication date: 2-Sep-2023
https://doi.org/10.1007/978-3-031-38499-8_22
Show More Cited By

Index Terms

Modal Resolution: Proofs, Layers, and Refinements
1. Theory of computation
  1. Logic
    1. Automated reasoning
    2. Modal and temporal logics

Recommendations

A Modal-Layered Resolution Calculus for K
TABLEAUX 2015: Proceedings of the 24th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods - Volume 9323

Resolution-based provers for multimodal normal logics require pruning of the search space for a proof in order to deal with the inherent intractability of the satisfiability problem for such logics. We present a clausal modal-layered hyper-resolution ...
Towards Resolution-based Reasoning for Connected Logics

The method of connecting logics has gained a lot of attention in the knowledge representation and ontology communities because of its intuitive semantics and natural support for modular KR, its generality, and its robustness concerning decidability ...
Clausal resolution for normal modal logics

We present a clausal resolution-based method for normal modal logics. Differently from other approaches, where inference rules are based on the syntax of a particular set of axioms, we focus on the restrictions imposed on the binary accessibility ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Transactions on Computational Logic

ACM Transactions on Computational Logic Volume 20, Issue 4

October 2019

323 pages

ISSN:1529-3785

EISSN:1557-945X

DOI:10.1145/3347091

Editor:
Orna Kupferman
School of Computer Science and Engineering, Hebrew University, Israel

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 13 August 2019

Accepted: 01 May 2019

Revised: 01 March 2019

Received: 01 December 2017

Published in TOCL Volume 20, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed

Funding Sources

Engineering and Physical Sciences Research Council

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

9
Total Citations
View Citations
636
Total Downloads

Downloads (Last 12 months)104
Downloads (Last 6 weeks)22

Reflects downloads up to 23 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Hustadt UPapacchini FNalon CDixon C(2024)Model Construction for Modal ClausesAutomated Reasoning10.1007/978-3-031-63501-4_1(3-23)Online publication date: 2-Jul-2024
https://doi.org/10.1007/978-3-031-63501-4_1
Pattinson DOlivetti NNalon C(2023)Resolution Calculi for Non-normal Modal LogicsAutomated Reasoning with Analytic Tableaux and Related Methods10.1007/978-3-031-43513-3_18(322-341)Online publication date: 14-Sep-2023
https://doi.org/10.1007/978-3-031-43513-3_18
Nalon CHustadt UPapacchini FDixon C(2023)Buy One Get 14 Free: Evaluating Local Reductions for Modal LogicAutomated Deduction – CADE 2910.1007/978-3-031-38499-8_22(382-400)Online publication date: 2-Sep-2023
https://doi.org/10.1007/978-3-031-38499-8_22
Dennis LDixon CFisher M(2022)Verifiable autonomy: From theory to applicationsAI Communications10.3233/AIC-22011535:4(421-431)Online publication date: 20-Sep-2022
https://doi.org/10.3233/AIC-220115
Papacchini FNalon CHustadt UDixon C(2022)Local is Best: Efficient Reductions to Modal Logic KJournal of Automated Reasoning10.1007/s10817-022-09630-666:4(639-666)Online publication date: 23-May-2022
https://doi.org/10.1007/s10817-022-09630-6
Nalon CHustadt UPapacchini FDixon C(2022)Local Reductions for the Modal CubeAutomated Reasoning10.1007/978-3-031-10769-6_29(486-505)Online publication date: 1-Aug-2022
https://doi.org/10.1007/978-3-031-10769-6_29
Sigley SBeyersdorff O(2021)Proof Complexity of Modal ResolutionJournal of Automated Reasoning10.1007/s10817-021-09609-9Online publication date: 13-Oct-2021
https://doi.org/10.1007/s10817-021-09609-9
Dixon C(2021)Theorem Proving Using Clausal Resolution: From Past to PresentReachability Problems10.1007/978-3-030-89716-1_2(19-27)Online publication date: 22-Oct-2021
https://doi.org/10.1007/978-3-030-89716-1_2
Papacchini FNalon CHustadt UDixon C(2021)Efficient Local Reductions to Basic Modal LogicAutomated Deduction – CADE 2810.1007/978-3-030-79876-5_5(76-92)Online publication date: 5-Jul-2021
https://doi.org/10.1007/978-3-030-79876-5_5

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

HTML Format

View this article in HTML Format.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents