Institute for Logic, Complexity and Deduction Systems, Department
of Computer Science, University of Karlsruhe There are no up-to-date text books out that cover the topic. What
comes closest is "First-Order Logic and Automated Theorem Proving"
by Melvin Fitting, 2nd ed., Springer-Verlag 1996. I will, however,
go deeper into computational aspects than Fitting who does not
discuss any refinements. The course is based on my lecture "Automated Theorem Proving"
held so far three times in Karlsruhe and an abridged version held
at TU Vienna last spring. You can get an impression by looking
at some of the coures materials at http://i12www.ira.uka.de/~reiner/courses.html which are currently in German. There is an overview article in
English which partly covers the course: http://i12www.ira.uka.de/~reiner/spp.ps.gz
Logic and Computation
TABLEAU-BASED THEOREM PROVING
Introductory course
First week
reiner@ira.uka.de
Course description
Tableau-based approaches to automated deduction have gained a
lot of ground in recent years after many years during which they
have been mainly considered for teaching and in proof theoretic
studies. One reason for this development is that competititve
implementations of FOL tableau provers are now available, but
another reason for the renewed interest is th large number of
applications for deduction in non-classical in linguistics, intelligent
agents, knowledge representation to name just a few fields. I
will present various tableau-related calculi in a uniform, modern
framework with new, concise completeness proofs. Important implementations
as well as basic techniques for accommodating non-classical aspects
are discussed as well. A brief introduction into the required
concepts of computational logic is included.
Prerequisites
None
Literature