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.
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.
Bidragets oversatte titel | Et Seligman Tableau System |
---|---|
Originalsprog | Engelsk |
Titel | Logic for Programming, Artificial Intelligence, and Reasoning |
Redaktører | Ken McMillan, Aart Middeldorp, Andrei Voronkov |
Antal sider | 16 |
Udgivelsessted | Heidelberg |
Forlag | Springer Publishing Company |
Publikationsdato | 2013 |
Sider | 147-163 |
ISBN (Trykt) | 978-3-642-45220-8 |
ISBN (Elektronisk) | 978-3-642-45221-5 |
Status | Udgivet - 2013 |
Begivenhed | 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning - Stellenbosch, Sydafrika Varighed: 14 dec. 2013 → 19 dec. 2013 Konferencens nummer: 19 http://www.lpar-19.info/ |
Konference
Konference | 19th International Conference on Logic for Programming, Artificial Intelligence and Reasoning |
---|---|
Nummer | 19 |
Land/Område | Sydafrika |
By | Stellenbosch |
Periode | 14/12/2013 → 19/12/2013 |
Internetadresse |
Navn | Lecture Notes in Computer Science |
---|---|
Vol/bind | 8312 |
ISSN | 0302-9743 |