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.

Pettorossi, A., Proietti, M. (2016). First order predicate calculus and logic programming. Fourth Edition. Roma : Aracne.

### 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 (à 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.
##### Scheda breve Scheda completa Scheda completa (DC)
Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni
English
Rilevanza internazionale
Manuale
first order predicate calculus; logic programming; resolution theorem proving
Pettorossi, A., Proietti, M. (2016). First order predicate calculus and logic programming. Fourth Edition. Roma : Aracne.
Monografia
Pettorossi, A; Proietti, M
File in questo prodotto:
File
101010PredCalc_Log.pdf

accesso solo dalla rete interna

Utilizza questo identificativo per citare o creare un link a questo documento: `http://hdl.handle.net/2108/184185`
• ND
• ND
• ND