Melvin C. Fitting: First-Order Logic and Automated Theorem Proving, 1996. Springer-Verlag, Berlin. ISBN: 0-387-94593-8. 2. utgave.
ERRATA A list of errors for the textbook.
Completeness for First-Order Tableaux, Compendium. ../completeness.pdf.
Göran Sundholm: Systems of Deduction, contained in the compendium "Kopisamling INF3170/4170 Logikk og analysemetoder" available at Kopiusalget, Akademika campus bookshop.
Detailed syllabus can be found by inspecting the teaching plan .
In addition come the obligatory exercises and the material presented at the lectures.