Ragionamento Automatico (DM 509)

Attenzione: Questo corso si è svolto nel anno accademico 2008/2009 per l'ultima volta. Il programma di Ragionamento Automatico sarà parzialmente coperto nel ambito del corso Knowledge Management.

Esami extra:

• 2009-12-09 09:00, MT6
  • registrazione 18/2/2010 17:00, nello studio del docente
• 2010-07-09 15:00, MT6
• 2010-09-27 09:00, MT6

Programma

1. Logica
   • Introduzione e cenni storici
   • Logica proposizionale
   • Logica del primo ordine
   • Logica proposizionale con quantificatori
2. Linguaggi logici per basi di dati
   • Logica del primo ordine come linguaggio di interrogazione per basi di dati
   • Datalog
   • Negazione come fallimento
   • Disgiunzione
   • Answer Set Programming
3. Pianificazione (facoltativamente)
   • Introduzione e cenni storici
   • Linguaggi di azione
   • Pianificazione can linguaggi di azione
   • Panoramica dei metodi risolutivi

Docente

• Wolfgang Faber

• Ricevimenti per Ragionamento Automatico: Martedì 17:00-18:00
• Studio: Cubo 30b, piano 2 (ponte coperto), prima porta a sinistra

Lucidi

1. Introduzione, introduzione-presentazione.pdf introduzione-stampabile.pdf

2. Logica Proposizionale, logica-proposizionale-presentazione.pdf logica-proposizionale-stampabile.pdf

3. Esercizi Logica Proposizionale, esercizi-logica-proposizionale-presentazione.pdf esercizi-logica-proposizionale-stampabile.pdf

4. Risoluzione Proposizionale, risoluzione-proposizionale-presentazione.pdf risoluzione-proposizionale-stampabile.pdf

5. DPLL ed Esercizi di Computazioni in Logica Proposizionale, DPLL-esercizi.pdf, DPLL-esercizi-stampabile.pdf

6. Esercizi sul Computer I, esercizi-logica-proposizionale-computer1.2.pdf esercizi-logica-proposizionale-computer1-stampabile.2.pdf

7. QSAT ed Esercizi, qbf-presentazione.pdf

8. Logica del Primo Ordine 1, logica-primo-ordine-1-presentazione.pdf logica-primo-ordine-1-stampabile.pdf

9. Logica del Primo Ordine 2, logica-primo-ordine-2-presentazione.1.pdf logica-primo-ordine-2-stampabil.1.pdf

10. Logica del Primo Ordine - Calcoli, logica-primo-ordine-calcoli-presentazione.3.pdf logica-primo-ordine-calcoli-stampabile.3.pdf

11. Logica e Basi di Dati - Calcolo Relazionale e Datalog, logica-basi-di-dati-presentazione.pdf, logica-basi-di-dati-stampabile.pdf

12. Datalog con Negazione, datalog-con-negazione-presentazione.pdf, datalog-con-negazione-handout.pdf

Libri

• Logica a Informatica Andrea Asperti, Agata Ciabattoni

  McGraw-Hill, 1997 ISBN: 88-386-0757-5

  ateneoonline

• Foundations of Databases Serge Abiteboul, Richard Hull, Victor Vianu Addison-Wesley, 1995 ISBN: 0-201-53771-0
• Logic for Computer Science: Foundations of Automatic Theorem Proving Jean Gallier Wiley, 1986

  online version

Pagine Web

• Applets per generare tabelle di verità, visualizzare formule come alberi, trasformazione in CNF, risoluzione assistita ecc.

• Applet per tabelle di verità, trasformazione in CNF ecc.

• Competizione di sistemi SAT

• SAT Live! -- notizie nell'ambito di SAT

• QBF Library

• QBF Evaluation

Sistemi

SAT

• MiniSat

• PicoSAT

QBF

• Quantor

• EBDDRES

• sKizzo

Primo Ordine

• Prover9

• Darwin

Software

• pigeonhole.pl

• pigeonhole-fixed.pl

• rip.pl

• qip.pl

Orario

1. 14/10/2008, 15:00-17:00
2. 15/10/2008, 15:00-17:00
3. 16/10/2008, 11:30-13:30
4. 21/10/2008, 15:00-17:00
5. 22/10/2008, 15:00-17:00
6. 23/10/2008, 11:30-13:30
7. 28/10/2008, 15:00-17:00
8. 29/10/2008, 15:00-17:00
9. 30/10/2008, 11:30-13:30
10. 04/11/2008, 9:30-11:30
11. 05/11/2008, 9:30-11:30
12. 06/11/2008, 11:30-13:30
13. 11/11/2008, 15:00-17:00
14. 12/11/2008, 15:00-17:00
15. 13/11/2008, 11:30-13:30
16. 18/11/2008, 15:00-17:00
17. 19/11/2008, 15:00-17:00
18. 20/11/2008, 11:30-13:30
19. 25/11/2008, 15:00-17:00
20. 26/11/2008, 15:00-17:00
21. 27/11/2008, 11:30-13:30
22. 02/12/2008, 15:00-17:00
23. 03/12/2008, 15:00-17:00
24. 04/12/2008, 11:30-13:30
25. 09/12/2008, 15:00-17:00 (riserva)
26. 10/12/2008, 15:00-17:00 (riserva)
27. 11/12/2008, 11:30-13:30 (riserva)

Aula

• Laboratorio, cubo 31a, primo piano

Esami

• 9/1/2009 9:00 MT6
  • registrazione 16/1/2009 10:00 e 21/1/2009 11:00, nello studio del docente
• Appello straordinario 5/2/2009 9:30 MT11 (cubo 30b, 1o piano)
  • registrazione 10/02/2009 17:00, nello studio del docente
• 7/7/2009 9:00 MT6
  • registrazione 7/7/2009 17:00, nello studio del docente
• 8/9/2009 9:00 Lab 31a
• 9/12/2009 9:00 MT6

L'esame si svolge come prova scritta.

Consulta le tracce vecchie.