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)
 Save to my reading list
Follow the author(s)
My bibliography
Export citation
Find it on Scholar
Edit this record
Mark as duplicate
Revision history
Request removal from index
Translate to english
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 26,173
External links

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.

Add more references

Citations of this work BETA

Add more citations

Similar books and articles

Monthly downloads

Added to index


Total downloads

14 ( #326,654 of 2,152,487 )

Recent downloads (6 months)


How can I increase my downloads?

My notes
Sign in to use this feature

There  are no threads in this forum
Nothing in this forum yet.

Other forums