A Seligman-Style Tableau System

Bidragets oversatte titel: Et Seligman Tableau System

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

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

Resumé

Abstract. Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labeling approach lies at the heart of the best known resolution, natural deduction, and tableau systems. The distinguishing feature of labeling systems is that they work only with satisfaction statements (that is, formulas preceded by an @) and a number of them have been successfully implemented. But there is another, less well-known 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 the setting of natural deduction and sequent calculus in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system.

The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just satisfaction statements. We capture this idea in the tableau setting by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. To the surprise of at least some of the authors (who have worked extensively on developing the labeling approach) the Seligman-style approach turns out to be conceptually clearer. Not only is the approach more modular than labeling, but individual proofs are often more revealing. This is partly because Seligman-style inference masks many irrelevant book-keeping details, and partly because the GoTo rule lets us structure arguments in a natural way.
OriginalsprogEngelsk
TitelLogic for Programming, Artificial Intelligence, and Reasoning
RedaktørerKen McMillan, Aart Middeldorp, Andrei Voronkov
Antal sider16
Udgivelses stedHeidelberg
ForlagSpringer Publishing Company
Publikationsdato2013
Sider147-163
ISBN (Trykt)978-3-642-45220-8
ISBN (Elektronisk)978-3-642-45221-5
StatusUdgivet - 2013
Begivenhed19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Stellenbosch, Sydafrika
Varighed: 14 dec. 201319 dec. 2013
Konferencens nummer: 19
http://www.lpar-19.info/

Konference

Konference19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Nummer19
LandSydafrika
ByStellenbosch
Periode14/12/201319/12/2013
Internetadresse
NavnLecture Notes in Computer Science
Vol/bind8312
ISSN0302-9743

Citer dette

Blackburn, P. R., Bolander, T., Braüner, T., & Jørgensen, K. F. (2013). A Seligman-Style Tableau System. I K. McMillan, A. Middeldorp, & A. Voronkov (red.), Logic for Programming, Artificial Intelligence, and Reasoning (s. 147-163). Heidelberg: Springer Publishing Company. Lecture Notes in Computer Science, Bind. 8312
Blackburn, Patrick Rowan ; Bolander, Thomas ; Braüner, Torben ; Jørgensen, Klaus Frovin. / A Seligman-Style Tableau System. Logic for Programming, Artificial Intelligence, and Reasoning. red. / Ken McMillan ; Aart Middeldorp ; Andrei Voronkov. Heidelberg : Springer Publishing Company, 2013. s. 147-163 (Lecture Notes in Computer Science, Bind 8312).
@inproceedings{58d66e0f19d64873b1b56f16fdc5381d,
title = "A Seligman-Style Tableau System",
abstract = "Abstract. Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labeling approach lies at the heart of the best known resolution, natural deduction, and tableau systems. The distinguishing feature of labeling systems is that they work only with satisfaction statements (that is, formulas preceded by an @) and a number of them have been successfully implemented. But there is another, less well-known 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 the setting of natural deduction and sequent calculus in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system.The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just satisfaction statements. We capture this idea in the tableau setting by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. To the surprise of at least some of the authors (who have worked extensively on developing the labeling approach) the Seligman-style approach turns out to be conceptually clearer. Not only is the approach more modular than labeling, but individual proofs are often more revealing. This is partly because Seligman-style inference masks many irrelevant book-keeping details, and partly because the GoTo rule lets us structure arguments in a natural way.",
author = "Blackburn, {Patrick Rowan} and Thomas Bolander and Torben Bra{\"u}ner and J{\o}rgensen, {Klaus Frovin}",
year = "2013",
language = "English",
isbn = "978-3-642-45220-8",
pages = "147--163",
editor = "Ken McMillan and Aart Middeldorp and Andrei Voronkov",
booktitle = "Logic for Programming, Artificial Intelligence, and Reasoning",
publisher = "Springer Publishing Company",
address = "United States",

}

Blackburn, PR, Bolander, T, Braüner, T & Jørgensen, KF 2013, A Seligman-Style Tableau System. i K McMillan, A Middeldorp & A Voronkov (red), Logic for Programming, Artificial Intelligence, and Reasoning. Springer Publishing Company, Heidelberg, Lecture Notes in Computer Science, bind 8312, s. 147-163, 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Stellenbosch, Sydafrika, 14/12/2013.

A Seligman-Style Tableau System. / Blackburn, Patrick Rowan; Bolander, Thomas; Braüner, Torben; Jørgensen, Klaus Frovin.

Logic for Programming, Artificial Intelligence, and Reasoning. red. / Ken McMillan; Aart Middeldorp; Andrei Voronkov. Heidelberg : Springer Publishing Company, 2013. s. 147-163 (Lecture Notes in Computer Science, Bind 8312).

Publikation: Bidrag til bog/antologi/rapportKonferencebidrag i proceedingsForskningpeer review

TY - GEN

T1 - A Seligman-Style Tableau System

AU - Blackburn, Patrick Rowan

AU - Bolander, Thomas

AU - Braüner, Torben

AU - Jørgensen, Klaus Frovin

PY - 2013

Y1 - 2013

N2 - Abstract. Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labeling approach lies at the heart of the best known resolution, natural deduction, and tableau systems. The distinguishing feature of labeling systems is that they work only with satisfaction statements (that is, formulas preceded by an @) and a number of them have been successfully implemented. But there is another, less well-known 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 the setting of natural deduction and sequent calculus in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system.The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just satisfaction statements. We capture this idea in the tableau setting by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. To the surprise of at least some of the authors (who have worked extensively on developing the labeling approach) the Seligman-style approach turns out to be conceptually clearer. Not only is the approach more modular than labeling, but individual proofs are often more revealing. This is partly because Seligman-style inference masks many irrelevant book-keeping details, and partly because the GoTo rule lets us structure arguments in a natural way.

AB - Abstract. Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labeling approach lies at the heart of the best known resolution, natural deduction, and tableau systems. The distinguishing feature of labeling systems is that they work only with satisfaction statements (that is, formulas preceded by an @) and a number of them have been successfully implemented. But there is another, less well-known 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 the setting of natural deduction and sequent calculus in the 1990s. The purpose of this paper is to introduce a Seligman-style tableau system.The most obvious feature of Seligman-style systems is that they work with arbitrary formulas, not just satisfaction statements. We capture this idea in the tableau setting by introducing a rule called GoTo which allows us to “jump to a named world” on a tableau branch. To the surprise of at least some of the authors (who have worked extensively on developing the labeling approach) the Seligman-style approach turns out to be conceptually clearer. Not only is the approach more modular than labeling, but individual proofs are often more revealing. This is partly because Seligman-style inference masks many irrelevant book-keeping details, and partly because the GoTo rule lets us structure arguments in a natural way.

M3 - Article in proceedings

SN - 978-3-642-45220-8

SP - 147

EP - 163

BT - Logic for Programming, Artificial Intelligence, and Reasoning

A2 - McMillan, Ken

A2 - Middeldorp, Aart

A2 - Voronkov, Andrei

PB - Springer Publishing Company

CY - Heidelberg

ER -

Blackburn PR, Bolander T, Braüner T, Jørgensen KF. A Seligman-Style Tableau System. I McMillan K, Middeldorp A, Voronkov A, red., Logic for Programming, Artificial Intelligence, and Reasoning. Heidelberg: Springer Publishing Company. 2013. s. 147-163. (Lecture Notes in Computer Science, Bind 8312).