Completeness and Termination for a Seligman-style Tableau System

Patrick Rowan Blackburn, Thomas Bolander, Torben Braüner, Klaus Frovin Jørgensen

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction, and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction [22] and sequent calculus [23] in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved constructively: we give trans- lations which transform tableaus in a standard labelled system into tableaus in our Seligman-system and vice-versa.
Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction, and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction [22] and sequent calculus [23] in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved constructively: we give trans- lations which transform tableaus in a standard labelled system into tableaus in our Seligman-system and vice-versa.
Translated title of the contributionFuldstændighed og termination for et Seligman-style tableau system :
LanguageEnglish
JournalJournal of Logic and Computation
Volume27
Issue number1
Pages81-107
ISSN0955-792X
DOIs
StatePublished - 2017

Cite this

@article{075ffd2a07b843029a9b8f8bfebdb240,
title = "Completeness and Termination for a Seligman-style Tableau System",
abstract = "Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction, and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction [22] and sequent calculus [23] in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved constructively: we give trans- lations which transform tableaus in a standard labelled system into tableaus in our Seligman-system and vice-versa.",
author = "Blackburn, {Patrick Rowan} and Thomas Bolander and Torben Bra{\"u}ner and J{\o}rgensen, {Klaus Frovin}",
year = "2017",
doi = "10.1093/logcom/exv052",
language = "English",
volume = "27",
pages = "81--107",
journal = "Journal of Logic and Computation",
issn = "0955-792X",
publisher = "Oxford University Press",
number = "1",

}

Completeness and Termination for a Seligman-style Tableau System. / Blackburn, Patrick Rowan; Bolander, Thomas; Braüner, Torben; Jørgensen, Klaus Frovin.

In: Journal of Logic and Computation, Vol. 27, No. 1, 2017, p. 81-107.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Completeness and Termination for a Seligman-style Tableau System

AU - Blackburn,Patrick Rowan

AU - Bolander,Thomas

AU - Braüner,Torben

AU - Jørgensen,Klaus Frovin

PY - 2017

Y1 - 2017

N2 - Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction, and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction [22] and sequent calculus [23] in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved constructively: we give trans- lations which transform tableaus in a standard labelled system into tableaus in our Seligman-system and vice-versa.

AB - Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labelling approach lies at the heart of the best known hybrid resolution, natural deduction, and tableau systems. But there is another approach, which we have come to believe is conceptually clearer. We call this Seligman-style inference, as it was first introduced and explored by Jerry Seligman in natural deduction [22] and sequent calculus [23] in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system, to prove its completeness, and to show how it can be made to terminate. The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just statements prefixed by @-operators. They do so by introducing machinery for switching to other proof contexts. We capture this idea in the setting of tableaus by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. We first develop a Seligman-style tableau system for basic hybrid logic and prove its completeness. We then prove termination of a restricted version of the system without resorting to loop checking, and show that the restrictions do not effect completeness. Both completeness and termination results are proved constructively: we give trans- lations which transform tableaus in a standard labelled system into tableaus in our Seligman-system and vice-versa.

U2 - 10.1093/logcom/exv052

DO - 10.1093/logcom/exv052

M3 - Journal article

VL - 27

SP - 81

EP - 107

JO - Journal of Logic and Computation

T2 - Journal of Logic and Computation

JF - Journal of Logic and Computation

SN - 0955-792X

IS - 1

ER -