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

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.
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). Springer Publishing Company. Lecture Notes in Computer Science, Bind. 8312