Implementing a relational theorem prover for modal logic

uncategorised

Authors

Ángel Mora

Emilio Muñoz Velasco

Joanna Golinska-Pilarek

Published

1 January 2011

Publication details

Int. J. Comput. Math. vol. 88 (9), pages 1869–1884.

Links

Abstract

An automatic theorem prover for a proof system in the style of dual tableaux for the relational logic associated with modal logic has been introduced. Although there are many well-known implementations of provers for modal logic, as far as we know, it is the first implementation of a specific relational prover for a standard modal logic. There are two main contributions in this paper. First, the implementation of new rules, called () and (), which substitute the classical relational rules for composition and negation of composition in order to guarantee not only that every proof tree is finite but also to decrease the number of applied rules in dual tableaux. Second, the implementation of an order of application of the rules which ensures that the proof tree obtained is unique. As a consequence, we have implemented a decision procedure for modal logic . Moreover, this work would be the basis for successive extensions of this logic, such as , and .

Citation

Please, cite this work as:

[MMG11] Á. Mora, E. Mu~noz-Velasco, and J. Golinska-Pilarek. “Implementing a relational theorem prover for modal logic”. In: Int. J. Comput. Math. 88.9 (2011), pp. 1869-1884. DOI: 10.1080/00207160.2010.493211. URL: https://doi.org/10.1080/00207160.2010.493211.

BibTeX

@Article{Mora2011a,
     author = {{’A}ngel Mora and Emilio Mu~noz-Velasco and Joanna Golinska-Pilarek},
     journal = {Int. J. Comput. Math.},
     title = {Implementing a relational theorem prover for modal logic},
     year = {2011},
     number = {9},
     pages = {1869–1884},
     volume = {88},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/ijcm/MoraMG11.bib},
     doi = {10.1080/00207160.2010.493211},
     timestamp = {Fri, 23 Sep 2022 01:00:00 +0200},
     url = {https://doi.org/10.1080/00207160.2010.493211},
}

Bibliometric data

The following data has been extracted from resources such as OpenAlex, Dimensions, PlumX or Altmetric.

Citations
CrossRef - Citation Indexes: 5
Scopus - Citation Indexes: 8

Captures
Mendeley - Readers: 4

Cites

The following graph plots the number of cites received by this work from its publication, on a yearly basis.

Papers citing this work

The following is a non-exhaustive list of papers that cite this work:

[1] A. Burrieza, E. Muñoz-Velasco, and M. Ojeda-Aciego. “Logics for Order-of-Magnitude Qualitative Reasoning: Formalizing Negligibility”. In: Ewa Orłowska on Relational Methods in Logic and Computer Science. Springer International Publishing, 2018, p. 203–231. ISBN: 9783319978796. DOI: 10.1007/978-3-319-97879-6_8. URL: http://dx.doi.org/10.1007/978-3-319-97879-6_8.

[2] D. Cantone, J. Golińska-Pilarek, and M. Nicolosi-Asmundo. “A Relational Dual Tableau Decision Procedure for Multimodal and Description Logics”. In: Hybrid Artificial Intelligence Systems. Springer International Publishing, 2014, p. 466–477. ISBN: 9783319076171. DOI: 10.1007/978-3-319-07617-1_41. URL: http://dx.doi.org/10.1007/978-3-319-07617-1_41.

[3] D. Cantone and M. Nicolosi-Asmundo. “Dual Tableau-Based Decision Procedures for Fragments of the Logic of Binary Relations”. In: Ewa Orłowska on Relational Methods in Logic and Computer Science. Springer International Publishing, 2018, p. 169–202. ISBN: 9783319978796. DOI: 10.1007/978-3-319-97879-6_7. URL: http://dx.doi.org/10.1007/978-3-319-97879-6_7.

[4] D. Cantone, M. Nicolosi-Asmundo, and E. Orłowska. A Dual Tableau-based Decision Procedure for a Relational Logic with the Universal Relation (Extended Version). 2018. DOI: 10.48550/ARXIV.1802.07508. URL: https://arxiv.org/abs/1802.07508.

[5] A. A. Da Silveira, R. Ribeiro, M. A. Nunes, et al. “A Sound Deep Embedding of Arbitrary Normal Modal Logics in Coq”. In: Proceedings of the XXVI Brazilian Symposium on Programming Languages. SBLP 2022. ACM, Oct. 2022, p. 1–7. DOI: 10.1145/3561320.3561329. URL: http://dx.doi.org/10.1145/3561320.3561329.

[6] J. Golińska-Pilarek, T. Huuskonen, and E. Muñoz-Velasco. “Relational dual tableau decision procedures and their applications to modal and intuitionistic logics”. In: Annals of Pure and Applied Logic 165.2 (Feb. 2014), p. 409–427. ISSN: 0168-0072. DOI: 10.1016/j.apal.2013.06.003. URL: http://dx.doi.org/10.1016/j.apal.2013.06.003.

[7] J. Golinska-Pilarek, E. Munoz-Velasco, and A. Mora-Bonilla. “Relational dual tableau decision procedure for modal logic K”. In: Logic Journal of IGPL 20.4 (Feb. 2011), p. 747–756. ISSN: 1368-9894. DOI: 10.1093/jigpal/jzr019. URL: http://dx.doi.org/10.1093/jigpal/jzr019.

[8] N. Madrid and M. Ojeda-Aciego. “On the existence and unicity of stable models in normal residuated logic programs”. In: International Journal of Computer Mathematics 89.3 (Feb. 2012), p. 310–324. ISSN: 1029-0265. DOI: 10.1080/00207160.2011.580842. URL: http://dx.doi.org/10.1080/00207160.2011.580842.

[9] J. Vigo-Aguiar and J. A. Lopez-Ramos. “Applications of computational mathematics in science and engineering”. In: International Journal of Computer Mathematics 88.9 (Jun. 2011), p. 1805–1807. ISSN: 1029-0265. DOI: 10.1080/00207160.2011.578828. URL: http://dx.doi.org/10.1080/00207160.2011.578828.