Logic for computer scientists (Q5905500)

(See also the review of the German original [Mannheim (1987; Zbl 0637.03002)].) This book concentrates on those aspects of mathematical logic which have strong connections with different topics in computer science, especially automated deduction, logic programming, program verification and semantics of programming languages. In the first chapter, the main concepts and results concerning propositional logic are introduced, emphasising some typical aspects related to resolution-based theorem proving. The fundamentals of predicate logic are presented in the next chapter; some specific aspects for computer science, such as undecidability, Herbrand theorem, the principle of Robinson resolution and some of its refinements, are developed to some extent. The third chapter of the book presents an introduction to the fascinating area of logic programming. Although it is not intended to be a first course in PROLOG, a well-founded theoretical framework for understanding logic programming is realised here. The main features of SLD-resolution are pointed out. The numerous exercises and illustrative examples contribute to a great extent to a better understanding of different concepts and results. The book can be successfully used as a handbook for an introductory course in artificial intelligence.