Melvin C. Fitting: First-Order Logic and Automated Theorem Proving, 1996. Springer-Verlag, Berlin. ISBN:?0-387-94593-8. 2. utgave.
Her finnes en ERRATA (oversikt over feil) til boken.
Det som er pensum er det er p? undervisningsplanen .
I tillegg er obligene og det som er gjennomg?tt p? forelesningene og gruppetimene pensum.
Spesielt: resolusjon er ikke pensum. Kun det av prolog som har blitt gjennomg?tt er pensum.