A new deduction system for deciding validity in modal logic {K}
Abstract
A new deduction system for deciding validity for the minimal decidable normal modal logic K is presented in this article. Modal logics could be very helpful in modelling dynamic and reactive systems such as bio-inspired systems and process algebras. In fact, recently the Connectionist Modal Logics has been presented, which combines the strengths of modal logics and neural networks. Thus, modal logic K is the basis for these approaches. Soundness, completeness and the fact that the system itself is a decision procedure are proved in this article. The main advantages of this approach are: first, the system is deterministic, i.e. it generates one proof tree for a given formula; second, the system is a validity-checker, hence it generates a proof of a formula (if such exists); and third, the language of deduction and the language of a logic coincide. Some of these advantages are compared with other classical approaches.
Citation
Please, cite this work as:
[GMM11] J. Golinska-Pilarek, E. Mu~noz-Velasco, and Á. Mora. “A new deduction system for deciding validity in modal logic K”. In: Log. J. IGPL 19.2 (2011), pp. 425-434. DOI: 10.1093/JIGPAL/JZQ033. URL: https://doi.org/10.1093/jigpal/jzq033.
Bibliometric data
The following data has been extracted from resources such as OpenAlex, Dimensions, PlumX or Altmetric.
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] E. Corchado and M. Wozniak. “Editorial: Neuro-symbolic Algorithms and Models for Bio-inspired Systems”. In: Logic Journal of IGPL 19.2 (Jul. 2010), p. 289–292. ISSN: 1368-9894. DOI: 10.1093/jigpal/jzq026. URL: http://dx.doi.org/10.1093/jigpal/jzq026.
[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.