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.
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