Relational dual tableau decision procedures and their applications to modal and intuitionistic logics

 

Abstract

We study a class DL of certain decidable relational logics of binary relations with a single relational constant and restricted composition. The logics in DL are defined in terms of semantic restrictions on the models. The main contribution of the present article is the construction of relational dual tableau decision procedures for the logics in DL. The systems are constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. All necessary bookkeeping is contained in the proof tree itself and used according to the explicit rules. All the systems are deterministic, producing exactly one proof tree for every formula. Furthermore, we show how the systems for logics in DL can be used as deterministic decision procedures for some modal and intuitionistic logics.

Citation

Please, cite this work as:

[GHM14] J. Golinska-Pilarek, T. Huuskonen, and E. Mu~noz-Velasco. “Relational dual tableau decision procedures and their applications to modal and intuitionistic logics”. In: Ann. Pure Appl. Log. 165.2 (2014), pp. 409-427. DOI: 10.1016/J.APAL.2013.06.003. URL: https://doi.org/10.1016/j.apal.2013.06.003.

BibTeX

@Article{GolinskaPilarek2014,
     author = {Joanna Golinska-Pilarek and Taneli Huuskonen and Emilio Mu~noz-Velasco},
     journal = {Ann. Pure Appl. Log.},
     title = {Relational dual tableau decision procedures and their applications to modal and intuitionistic logics},
     year = {2014},
     number = {2},
     pages = {409–427},
     volume = {165},
     bibsource = {dblp computer science bibliography, https://dblp.org},
     biburl = {https://dblp.org/rec/journals/apal/Golinska-PilarekHM14.bib},
     doi = {10.1016/J.APAL.2013.06.003},
     timestamp = {Fri, 21 Feb 2020 00:00:00 +0100},
     url = {https://doi.org/10.1016/j.apal.2013.06.003},
}

Bibliometric data

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

6

CITATIONS

6 Total citations

0 Recent citations

3.34 Field Citation Ratio

n/a Relative Citation Ratio

• Citations
• CrossRef - Citation Indexes: 6
• Scopus - Citation Indexes: 8

• Captures
• Mendeley - Readers: 6

-

see details

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] J. Golińska-Pilarek, E. Muñoz-Velasco, and A. Mora. “Tableau reductions: Towards an optimal decision procedure for the modal necessity”. In: Journal of Applied Logic 17 (Sep. 2016), p. 14–24. ISSN: 1570-8683. DOI: 10.1016/j.jal.2015.09.005. URL: http://dx.doi.org/10.1016/j.jal.2015.09.005.

[6] A. Grzelak and D. Leszczyńska-Jasion. “Automatic proof generation in an axiomatic system for $\mathsfCPL$ by means of the method of Socratic proofs”. In: Logic Journal of the IGPL 26.1 (Nov. 2017), p. 109–148. ISSN: 1368-9894. DOI: 10.1093/jigpal/jzx057. URL: http://dx.doi.org/10.1093/jigpal/jzx057.

[7] D. Leszczyńska-Jasion, M. Ignaszak, and S. Chlebowski. “Rasiowa–Sikorski Deduction Systems with the Rule of Cut: A Case Study”. In: Studia Logica 107.2 (Apr. 2018), p. 313–349. ISSN: 1572-8730. DOI: 10.1007/s11225-018-9795-7. URL: http://dx.doi.org/10.1007/s11225-018-9795-7.