×

Symmetries in modal logics. (English) Zbl 1372.03036

Summary: In this paper we develop the theoretical foundations to exploit symmetries in modal logics. We generalize the notion of symmetries of propositional formulas in conjunctive normal form to modal formulas using the framework provided by coinductive modal models introduced in [the first author and D. Gorín, J. Appl. Log. 8, No. 4, 305–318 (2010; Zbl 1215.03031)]. Hence, the results apply to a wide class of modal logics including, for example, hybrid logics. We present two graph constructions that enable the reduction of symmetry detection in modal formulas to the graph automorphism detection problem, and we evaluate the graph constructions on modal benchmarks.

MSC:

03B45 Modal logic (including the logic of norms)
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
68T27 Logic in artificial intelligence

Citations:

Zbl 1215.03031
PDFBibTeX XMLCite
Full Text: DOI arXiv

References:

[1] DOI: 10.1109/TC.2006.75 · doi:10.1109/TC.2006.75
[2] DOI: 10.1007/978-3-642-03359-9_3 · Zbl 1252.68254 · doi:10.1007/978-3-642-03359-9_3
[3] DOI: 10.1109/TCAD.2003.816218 · Zbl 05447143 · doi:10.1109/TCAD.2003.816218
[4] A First Course in Abstract Algebra (2003)
[5] Proceedings of the 40th Annual Design Automation Conference pp 836– (2003)
[6] Proceedings of the Sixth International Conference on Artificial Intelligence Planning Systems (AIPS) (Toulouse, France) pp 83– (2002)
[7] The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT 2004) Online Proceedings (Vancouver, BC, Canada) pp 257– (2004)
[8] Handbook of Satisfiability pp 289– (2009)
[9] Proceedings of the 20th International Joint Conference on Artificial Intelligence (IJCAI 2007) (Hyderabad, India) pp 2262– (2007)
[10] Proceedings of 18th International Conference on Computer Aided Verification (CAV 2006) (Seattle, WA, USA) 4144 pp 467– (2006)
[11] Journal of Artificial Intelligence Research, 18 pp 351– (2003)
[12] Proceedings of the Sixteenth International Joint Conference on Artificial Intelligence (IJCAI 99) (Stockholm, Sweden) pp 956– (1999)
[13] Proceedings of Formal Methods, International Symposium of Formal Methods Europe (FM 2005) (Newcastle, UK) 3582 pp 481– (2005) · Zbl 1078.68005
[14] Ph.D. Thesis (2007)
[15] Proceedings of 23rd International Conference on Automated Deduction (CADE-23) (Wroclaw, Poland) 6803 pp 222– (2011) · Zbl 1218.68006
[16] Symmetry. Cultural-historical and Ontological Aspects of Science-Arts Relations. The Natural and Man-Made World in an Interdisciplinary Approach (2007)
[17] Proceedings of the Fifth International Conference on Principles of Knowledge Representation and Reasoning (KR’96) (Cambridge, Massachusetts, USA) pp 148– (1996)
[18] Proceedings of AAAI Workshop on Tractable Reasoning (San Jose, CA) pp 17– (1992)
[19] Proceedings of the 21st International Joint Conference on Artificial Intelligence (IJCAI 2009) (Pasadena, California, USA) pp 721– (2009)
[20] Principles and Practice of Constraint Programming pp 17– (2005)
[21] DOI: 10.1007/BF00625969 · Zbl 05475431 · doi:10.1007/BF00625969
[22] Applied Algebra, Algebraic Algorithms and Error-correcting Codes pp 99– (1989)
[23] DOI: 10.1007/s100090200074 · Zbl 02178179 · doi:10.1007/s100090200074
[24] Handbook of Modal Logic 3 (2006)
[25] Modal Logic (2001) · Zbl 0998.03015
[26] DOI: 10.1007/BF00881844 · Zbl 0804.68134 · doi:10.1007/BF00881844
[27] Proceedings of 11th International Conference on Automated Deduction (CADE-11) (Saratoga Springs, NY, USA) 607 pp 281– (1992)
[28] Proceedings of the 22nd IEEE International Conference on Tools with Artificial Intelligence (ICTAI 2010) (Arras, France) 1 pp 329– (2010)
[29] DOI: 10.1023/A:1006249507577 · Zbl 0955.03013 · doi:10.1023/A:1006249507577
[30] DOI: 10.1145/350887.350891 · doi:10.1145/350887.350891
[31] ACM Computing Surveys, 38 (2006)
[32] DOI: 10.1007/s10107-003-0394-6 · Zbl 1082.90070 · doi:10.1007/s10107-003-0394-6
[33] Proceedings of Workshop on Symmetry and Constraint Satisfaction Problems - Affiliated to CP (SymCon) (Providence, RI, USA) (2007)
[34] DOI: 10.1007/s10107-002-0358-2 · Zbl 1023.90088 · doi:10.1007/s10107-002-0358-2
[35] Formal Techniques for Networked and Distributed Sytems (FORTE 2002) pp 243– (2002)
[36] Acta Informatica 22 pp 253– (1985)
[37] Handbook of Modal Logics pp 821– (2006)
[38] DOI: 10.1016/j.tcs.2015.06.020 · Zbl 1332.68200 · doi:10.1016/j.tcs.2015.06.020
[39] Proceedings of the Workshop on Algorithm Engineering and Experiments (ALENEX 2007) (New Orleans, Louisiana, USA) 7 pp 135– (2007)
[40] DOI: 10.1016/j.jal.2010.08.010 · Zbl 1215.03031 · doi:10.1016/j.jal.2010.08.010
[41] DOI: 10.1007/BF00625968 · Zbl 05475430 · doi:10.1007/BF00625968
[42] Proceedings of ECAI 2000 (Berlin, Germany) pp 199– (2000)
[43] Handbook of Constraint Programming pp 329– (2006) · Zbl 1175.90011
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.