Gentzen-type systems, resolution and tableaux

Journal of Automated Reasoning 10:265-281 (1993)
  Copy   BIBTEX

Abstract

In advanced books and courses on logic (e.g. Sm], BM]) Gentzen-type systems or their dual, tableaux, are described as techniques for showing validity of formulae which are more practical than the usual Hilbert-type formalisms. People who have learnt these methods often wonder why the Automated Reasoning community seems to ignore them and prefers instead the resolution method. Some of the classical books on AD (such as CL], Lo]) do not mention these methods at all. Others (such as Ro]) do, but the connections and reasons for preference remain unclear after reading them (at least to the present author, and obviously also the authors of OS], in which a theorem-prover, based exclusively on tableaux, is described). The confusion becomes greater when the reader is introduced to Kowalski's form of a clause ( Ko], Bu]), which is nothing but a Gentzen's sequent of atomic formulae, and when he realizes that resolution is just a form of a Cut, and so that while the elimination of cuts is the principal tool in proof-theory, its use is the main technique in AD!

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,221

External links

  • This entry has no external links. Add one.
Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Analytics

Added to PP
2009-04-13

Downloads
14 (#842,910)

6 months
0

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Arnon Avron
Tel Aviv University

Citations of this work

A note on cut-elimination for classical propositional logic.Gabriele Pulcini - 2022 - Archive for Mathematical Logic 61 (3):555-565.
Paraconsistency, paracompleteness, Gentzen systems, and trivalent semantics.Arnon Avron - 2014 - Journal of Applied Non-Classical Logics 24 (1-2):12-34.
Modal Hybrid Logic.Andrzej Indrzejczak - 2007 - Logic and Logical Philosophy 16 (2-3):147-257.

View all 14 citations / Add more citations

References found in this work

No references found.

Add more references