Libri di Testo:

• Programmazione logica e Prolog
• Marta Cialdea Mayer. Logica - Linguaggio, Ragionamento, Calcolo. Progetto Leonardo. Società Editrice Esculapio, 2002.
  www.inf.uniroma3.it/cialdea/teaching/ai/ai.html

•  Logica temporale, Model cheking ed SMV (Symbolic Model Verifier)
• Michael Huth and Mark Ryan. Logic in ComputerScience: modelling and reasoning about systems (2nd edition). Cambridge University Press

•  Verifica deduttiva e PVS (Proof Verification System)
  
• Doron Peled. Software Reliability Methods. Springer-Verlag
  

Materiale Didattico:

• introduzione al corso
  

• richiami sulla Logica Proposizionale (gentile concessione della Prof. Marta Cialdea)
• richiami sulla Logica dei Predicati        "
• deduzione automatica
  
• unificazione
  
• risoluzione
• PVS :  introduzione ed esempi di teorie
• Prolog_1
• un compilatore Prolog (Free Software):  SWI-Prolog
• Prolog: rappresentazione della conoscenza
• Prolog: strutture di controllo
• Prolog: operatore di taglio e negazione
  
• Prolog: predicati di controllo
• Prolog: manipolazione di DB
• esercizi Prolog
  

Prove di verifica: