First order predicate calculus and logic programming. Fourth Edition

These lecture notes are intended to introduce the reader to the basic notions of the first order predicate calculus and logic programming. We present the axioms and the inference rules of the first order predicate calculus in 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 following Tarski's approach. The Skolem Theorem, the Herbrand Theorem, and the Robinson Theorem are the three steps which lead us to the study of the Definite Logic programs. For these programs we give the denotational semantics via the least Herbrand models, the fixpoint semantics via the so called T_P operator, and the operational semantics via SLD trees. Finally, we consider the issue of deriving negative information from Definite Logic programs, and we present the theory of normal programs and the theory of programs as conjunctions of statements. Sections are devoted to the Gödel Completeness Theorem, the first order predicate calculus with equality, and the Peano Arithmetic.