Logic for applications

Anil Nerode's text walks readers through three families of logic: classical, intuitionistic and modal. Its central idea is that deduction can be understood as computation, so it looks closely at the logical and mathematical groundwork behind resolution theorem proving and logic programming. The authors frame these topics as central to computer science and artificial intelligence.

The coverage includes soundness, completeness and undecidability across classical, nonclassical and computation-based systems, along with compactness and the Herbrand and Skolem-Löwenheim theorems. For PROLOG, the book examines termination, negation as failure, and how these connect to nonmonotonic reasoning.

Written for advanced undergraduates and beginning graduate students in computer science or mathematics, it works well as a course text on classical and nonclassical logic and on logic programming. A historical appendix and a substantial list of references for further reading are included, and no advanced mathematics is assumed.