First Order Predicate Calculus And Logic Programming

This book introduces the reader to the first order predicate calculus and the basic notions of logic programming. We present the axioms and the inference rules of the first order predicate calculus according to two different styles: (i) the classical style à la Hilbert, and (ii) the Natural Deduction style à la Gentzen. We also present the semantics of this calculus by following Tarski’s approach. The theorems by Skolem, Herbrand, and Robinson are the three steps which lead the reader to the theory of logic programming. We first consider the class of definite logic programs and for these programs we give the model–theoretic, the fixpoint, and the operational semantics. These three semantics provide a way of deriving positive information from definite logic programs. We then consider the issue of deriving negative information from logic programs and we present the negation–as–failure rule, the theory of normal programs, and the theory of programs which can be any first order predicate calculus formula. In this book we also consider the first order predicate calculus with equality, we introduce Peano Arithmetic, and we briefly illustrate Gödel’s Completeness and Incom­pleteness theorems.