| [Sti87] |
An introduction to automated deduction
by Mark. E. Stickel. In W. Bibel and P. Jorrand editors, Fundamentals of Artificial Intelligence, Vol 232 of Lecture Notes in Computer Science, Springer, 1987
|
| [EisOhl93] |
Deduction systems based on resolution
by N. Eisinger and H. J. Ohlbach. In J. A. Robinson et al. editors, Handbook of Logic in Artificial Intelligence and Logic Programming vol. 1 Oxford University Press, 1993.
|
| [HBAR01] |
Handbook of Automated Reasoning
by Alan Robinson and Andrei Voronkov, editors. Elsevier Science B.V., 2001.
|
| [Lei97] |
The Resolution Calculus
by Alexander Leitsch. Texts in Theoretical Computer Science, An EATCS Series, Springer, 1997.
|
| [Fit96] |
First-Order Logic and Automated Theorem Proving
by Melving Fitting, Graduate Texts in Computer Science, Springer, 1996.
|
| [ChaLee73] |
Symbolic Logic and Mechanical Theorem Proving
by Chin-Liang Chang and Richard Char-Tung Lee. Computer Science Classics, Academic Press, 1973.
|
| [Ohl97] |
Introductory Logic Course Notes
by H. J. Ohlbach. Lecture Notes, Imperial College, London, 1997 (see also related slides).
|
| [Sti87] |
Tableaux and related methods
by Reiner Hähnle. In Robinson and Voronkov editors [HBAR01], Elsevier Science B.V., 2001.
|