Free-variable tableaux for propositional modal logics

Bernhard Beckert; Rajeev Goré

doi:10.1023/A:1013886427723

Free-variable tableaux for propositional modal logics

Bernhard Beckert^*, Rajeev Goré

^*Corresponding author for this work

Research output: Contribution to journal › Article › peer-review

11 Citations (Scopus)

Abstract

Free-variable semantic tableaux are a well-established technique for firstorder theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.

Original language	English
Pages (from-to)	59-96
Number of pages	38
Journal	Studia Logica
Volume	69
Issue number	1
DOIs	https://doi.org/10.1023/A:1013886427723
Publication status	Published - 2001

Access to Document

10.1023/A:1013886427723

Cite this

@article{f93380a8cbd547ac9e4b43f3c347e710,

title = "Free-variable tableaux for propositional modal logics",

abstract = "Free-variable semantic tableaux are a well-established technique for firstorder theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.",

keywords = "Automated deduction, Free-variable tableaux, Modal logics, Modal theorem proving",

author = "Bernhard Beckert and Rajeev Gor{\'e}",

year = "2001",

doi = "10.1023/A:1013886427723",

language = "English",

volume = "69",

pages = "59--96",

journal = "Studia Logica",

issn = "0039-3215",

publisher = "Springer Netherlands",

number = "1",

}

TY - JOUR

T1 - Free-variable tableaux for propositional modal logics

AU - Beckert, Bernhard

AU - Goré, Rajeev

PY - 2001

Y1 - 2001

N2 - Free-variable semantic tableaux are a well-established technique for firstorder theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.

AB - Free-variable semantic tableaux are a well-established technique for firstorder theorem proving where free variables act as a meta-linguistic device for tracking the eigenvariables used during proof search. We present the theoretical foundations to extend this technique to propositional modal logics, including non-trivial rigorous proofs of soundness and completeness, and also present various techniques that improve the efficiency of the basic naive method for such tableaux.

KW - Automated deduction

KW - Free-variable tableaux

KW - Modal logics

KW - Modal theorem proving

UR - http://www.scopus.com/inward/record.url?scp=18944398578&partnerID=8YFLogxK

U2 - 10.1023/A:1013886427723

DO - 10.1023/A:1013886427723

M3 - Article

SN - 0039-3215

VL - 69

SP - 59

EP - 96

JO - Studia Logica

JF - Studia Logica

IS - 1

ER -

Free-variable tableaux for propositional modal logics

Abstract

Access to Document

Other files and links

Fingerprint

Cite this