## page was renamed from Ragionamento Automatico #acl WolfgangFaber:read,write,revert EditorsGroup:read,write,delete,admin,revert All:read == 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 === * [[http://www.wfaber.com|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, [[attachment:introduzione-presentazione.pdf]] [[attachment:introduzione-stampabile.pdf]] 2. Logica Proposizionale, [[attachment:logica-proposizionale-presentazione.pdf]] [[attachment:logica-proposizionale-stampabile.pdf]] 3. Esercizi Logica Proposizionale, [[attachment:esercizi-logica-proposizionale-presentazione.pdf]] [[attachment:esercizi-logica-proposizionale-stampabile.pdf]] 4. Risoluzione Proposizionale, [[attachment:risoluzione-proposizionale-presentazione.pdf]] [[attachment:risoluzione-proposizionale-stampabile.pdf]] 5. DPLL ed Esercizi di Computazioni in Logica Proposizionale, [[attachment:DPLL-esercizi.pdf]], [[attachment:DPLL-esercizi-stampabile.pdf]] 6. Esercizi sul Computer I, [[attachment:esercizi-logica-proposizionale-computer1.2.pdf]] [[attachment:esercizi-logica-proposizionale-computer1-stampabile.2.pdf]] 7. QSAT ed Esercizi, [[attachment:qbf-presentazione.pdf]] 8. Logica del Primo Ordine 1, [[attachment:logica-primo-ordine-1-presentazione.pdf]] [[attachment:logica-primo-ordine-1-stampabile.pdf]] 9. Logica del Primo Ordine 2, [[attachment:logica-primo-ordine-2-presentazione.1.pdf]] [[attachment:logica-primo-ordine-2-stampabil.1.pdf]] 10. Logica del Primo Ordine - Calcoli, [[attachment:logica-primo-ordine-calcoli-presentazione.3.pdf]] [[attachment:logica-primo-ordine-calcoli-stampabile.3.pdf]] 11. Logica e Basi di Dati - Calcolo Relazionale e Datalog, [[attachment:logica-basi-di-dati-presentazione.pdf]], [[attachment:logica-basi-di-dati-stampabile.pdf]] 12. Datalog con Negazione, [[attachment:datalog-con-negazione-presentazione.pdf]], [[attachment:datalog-con-negazione-handout.pdf]] === Libri === * Logica a Informatica Andrea Asperti, Agata Ciabattoni Mc``Graw-Hill, 1997 ISBN: 88-386-0757-5 [[http://www.ateneonline.it/LibroAteneo.asp?item_id=914|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 [[http://www.cis.upenn.edu/~jean/gbooks/logic.html|online version]] === Pagine Web === * [[http://www.inf.unibz.it/~nutt/Proplog/|Applets per generare tabelle di verità, visualizzare formule come alberi, trasformazione in CNF, risoluzione assistita ecc.]] * [[http://www.oursland.net/aima/propositionApplet.html|Applet per tabelle di verità, trasformazione in CNF ecc.]] * [[http://www.satcompetition.org/|Competizione di sistemi SAT]] * [[http://www.satlive.org/|SAT Live! -- notizie nell'ambito di SAT]] * [[http://www.qbflib.org/|QBF Library]] * [[http://www.qbflib.org/qbfeval|QBF Evaluation]] === Sistemi === ==== SAT ==== * [[http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/MiniSat.html|MiniSat]] * [[http://fmv.jku.at/picosat/|PicoSAT]] ==== QBF ==== * [[http://fmv.jku.at/quantor/|Quantor]] * [[http://fmv.jku.at/ebddres/|EBDDRES]] * [[http://skizzo.info/|sKizzo]] ==== Primo Ordine ==== * [[http://www.cs.unm.edu/~mccune/prover9/|Prover9]] * [[http://combination.cs.uiowa.edu/Darwin/|Darwin]] === Software === * [[attachment:pigeonhole.pl]] * [[attachment:pigeonhole-fixed.pl]] * [[attachment:rip.pl]] * [[attachment: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 [[../RagionamentoAutomaticoDM509/TracceVecchie|tracce vecchie]].