Relational dual tableau decision procedure for modal logic K

Logic Journal of the IGPL 20 (4):747-756 (2012)
  Copy   BIBTEX

Abstract

We present a dual tableau system, RLK, which is itself a deterministic decision procedure verifying validity of K-formulas. The system is constructed in the framework of the original methodology of relational proof systems, determined only by axioms and inference rules, without any external techniques. Furthermore, we describe an implementation of the system RLK in Prolog, and we show some of its advantages.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,873

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Implementing a relational theorem prover for modal logic K.Angel Mora, Emilio Munoz Velasco & Joanna Golińska-Pilarek - 2011 - International Journal of Computer Mathematics 88 (9):1869-1884.
Relational dual tableaux for interval temporal logics.David Bresolin, Joanna Golinska-Pilarek & Ewa Orlowska - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):251–277.
Reasoning with Qualitative Velocity: Towards a Hybrid Approach.Joanna Golinska-Pilarek & Emilio Munoz Velasco - 2012 - In Emilio Corchado, Vaclav Snasel, Ajith Abraham, Michał Woźniak, Manuel Grana & Sung-Bae Cho (eds.), Hybrid Artificial Intelligent Systems. Springer. pp. 635--646.
Modal tableaux for reasoning about diagrams.Luis Fariñas del Cerro & Olivier Gasquet - 2006 - Poznan Studies in the Philosophy of the Sciences and the Humanities 91 (1):169-184.
Relational proof systems for spatial reasoning.Joanna Golińska-Pilarek & Ewa Orlowska - 2006 - Journal of Applied Non-Classical Logics 16 (3-4):409-431.

Analytics

Added to PP
2013-02-16

Downloads
42 (#388,607)

6 months
5 (#703,368)

Historical graph of downloads
How can I increase my downloads?

Author Profiles

Emilio Muñoz-Velasco
Universidad de Málaga
Joanna Golinska-Pilarek
University of Warsaw

References found in this work

No references found.

Add more references