Implementing a relational theorem prover for modal logic K

International Journal of Computer Mathematics 88 (9):1869-1884 (2011)
  Copy   BIBTEX

Abstract

An automatic theorem prover for a proof system in the style of dual tableaux for the relational logic associated with modal logic K 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 (k1) and (k2), 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 K. Moreover, this work would be the basis for successive extensions of this logic, such as T, B and S4.

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

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

Identity in modal logic theorem proving.Francis J. Pelletier - 1993 - Studia Logica 52 (2):291 - 308.
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.

Analytics

Added to PP
2013-02-16

Downloads
29 (#472,224)

6 months
2 (#658,980)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Joanna Golinska-Pilarek
University of Warsaw

References found in this work

No references found.

Add more references