Title: First order predicate calculus and logic programming. Fourth Edition
Abstract: 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 (a la Hilbert),
and (ii) the Natural Deduction style (a 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 Godel Completeness Theorem, the first order
predicate calculus with equality, and the Peano Arithmetic.
Publication Year: 2005
Publication Date: 2005-01-01
Language: en
Type: article
Access and Citation
AI Researcher Chatbot
Get quick answers to your questions about the article from our AI researcher chatbot