Gentzen-type systems, resolution and tableaux
David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
No categories specified
(categorize this paper)
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library||
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Marcello D'Agostino (1992). Are Tableaux an Improvement on Truth-Tables? Journal of Logic, Language and Information 1 (3):235-252.
Arnon Avron (1990). Relevance and Paraconsistency---A New Approach. II. The Formal Systems. Notre Dame Journal of Formal Logic 31 (2):169-202.
Anita Wasilewska (1984). DFC-Algorithms for Suszko Logic and One-to-One Gentzen Type Formalizations. Studia Logica 43 (4):395 - 404.
Tsutomu Hosoi (1988). Gentzen-Type Formulation of the Prepositional Logic LQ. Studia Logica 47 (1):41 - 48.
Peter Schroeder-Heister (2002). Resolution and the Origins of Structural Reasoning: Early Proof-Theoretic Ideas of Hertz and Gentzen. Bulletin of Symbolic Logic 8 (2):246-265.
Noriko H. Arai, Toniann Pitassi & Alasdair Urquhart (2006). The Complexity of Analytic Tableaux. Journal of Symbolic Logic 71 (3):777 - 790.
Francis Jeffry Pelletier (1998). Automated Natural Deduction in Thinker. Studia Logica 60 (1):3-43.
Grigori Mints (1993). Resolution Calculus for the First Order Linear Logic. Journal of Logic, Language and Information 2 (1):59-83.
Added to index2009-04-13
Total downloads14 ( #115,807 of 1,102,753 )
Recent downloads (6 months)0
How can I increase my downloads?