Gentzen-type systems, resolution and tableaux
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!
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
Relative Efficiency of Propositional Proof Systems: Resolution Vs. Cut-Free LK.Noriko H. Arai - 2000 - Annals of Pure and Applied Logic 104 (1-3):3-16.
Similar books and articles
Are Tableaux an Improvement on Truth-Tables?Marcello D'Agostino - 1992 - Journal of Logic, Language and Information 1 (3):235-252.
DFC-Algorithms for Suszko Logic and One-to-One Gentzen Type Formalizations.Anita Wasilewska - 1984 - Studia Logica 43 (4):395 - 404.
Gentzen-Type Formulation of the Prepositional Logic LQ.Tsutomu Hosoi - 1988 - Studia Logica 47 (1):41 - 48.
Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen.Peter Schroeder-Heister - 2002 - Bulletin of Symbolic Logic 8 (2):246-265.
The Complexity of Analytic Tableaux.Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart - 2006 - Journal of Symbolic Logic 71 (3):777 - 790.
Resolution Calculus for the First Order Linear Logic.Grigori Mints - 1993 - Journal of Logic, Language and Information 2 (1):59-83.
Added to index2009-04-13
Total downloads14 ( #326,654 of 2,152,487 )
Recent downloads (6 months)0
How can I increase my downloads?