A Seligman-Style Tableau System

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

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

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.
Translated title of the contributionEt Seligman Tableau System
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning
EditorsKen McMillan, Aart Middeldorp, Andrei Voronkov
Number of pages16
Place of PublicationHeidelberg
PublisherSpringer Publishing Company
Publication date2013
Pages147-163
ISBN (Print)978-3-642-45220-8
ISBN (Electronic)978-3-642-45221-5
Publication statusPublished - 2013
Event19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Stellenbosch, South Africa
Duration: 14 Dec 201319 Dec 2013
Conference number: 19
http://www.lpar-19.info/

Conference

Conference19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning
Number19
CountrySouth Africa
CityStellenbosch
Period14/12/201319/12/2013
Internet address
SeriesLecture Notes in Computer Science
Volume8312
ISSN0302-9743

Cite this

Blackburn, P. R., Bolander, T., Braüner, T., & Jørgensen, K. F. (2013). A Seligman-Style Tableau System. In K. McMillan, A. Middeldorp, & A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning (pp. 147-163). Heidelberg: Springer Publishing Company. Lecture Notes in Computer Science, Vol.. 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. editor / Ken McMillan ; Aart Middeldorp ; Andrei Voronkov. Heidelberg : Springer Publishing Company, 2013. pp. 147-163 (Lecture Notes in Computer Science, Vol. 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. in K McMillan, A Middeldorp & A Voronkov (eds), Logic for Programming, Artificial Intelligence, and Reasoning. Springer Publishing Company, Heidelberg, Lecture Notes in Computer Science, vol. 8312, pp. 147-163, Stellenbosch, South Africa, 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. ed. / Ken McMillan; Aart Middeldorp; Andrei Voronkov. Heidelberg : Springer Publishing Company, 2013. p. 147-163.

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-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. In McMillan K, Middeldorp A, Voronkov A, editors, Logic for Programming, Artificial Intelligence, and Reasoning. Heidelberg: Springer Publishing Company. 2013. p. 147-163. (Lecture Notes in Computer Science, Vol. 8312).