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

Proof systems for hybrid logic typically use @-operators to access information hidden behind modalities; this labeling approach lies at the heart of most resolution, natural deduction, and tableau systems for hybrid logic. 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 late 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 formulas prefixed by @-operators. To achieve this in a tableau system, we introduce a rule called GoTo which allows us to “jump to a named world” on a tableau branch, thereby creating a local proof context (which we call a block) on that branch. To the surprise of some of the authors (who have worked extensively on developing the labeling approach) Seligman-style inference is often clearer: not only is the approach more modular, individual proofs can be more direct. We briefly discuss termination and extensions to richer logics, and relate our system to Seligman’s original sequent calculus.
Original languageEnglish
Title of host publicationLogic for Programming, Artificial Intelligence, and Reasoning : 19th International Conference, LPAR-19, Stellenbosch, South Africa, December 14-19, 2013. Proceedings
PublisherSpringer
Publication date2013
Pages147-163
ISBN (Print)978-3-642-45220-8
ISBN (Electronic)978-3-642-45221-5
DOIs
Publication statusPublished - 2013
Event19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013) - Stellenbosch, South Africa
Duration: 14 Dec 201319 Dec 2013
http://www.lpar-19.info/

Conference

Conference19th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning (LPAR 2013)
Country/TerritorySouth Africa
CityStellenbosch
Period14/12/201319/12/2013
Internet address

Fingerprint

Dive into the research topics of 'A Seligman-Style Tableau System'. Together they form a unique fingerprint.

Cite this