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

PETTOROSSI, ALBERTO;
2016-01-01

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.
2016
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 Dimensione Formato  
101010PredCalc_Log.pdf

solo utenti autorizzati

Licenza: Copyright dell'editore
Dimensione 224.77 kB
Formato Adobe PDF
224.77 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2108/184185
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus ND
  • ???jsp.display-item.citation.isi??? ND
social impact