Logica e Sistemi Informatici

Avvisi:

• La lezione del 23 aprile è annullata. Ci sarà invece lezione martedì 22 aprile, dalle 9.45 alle 11.15, sempre in aula N3.
  
  
• Prenotazioni per gli esami:
  Per prenotarsi alla prima prova, gli studenti devono riempire l'apposito modulo, almeno 5 giorni prima della data della prova.
  Attenzione: saranno ammessi a sostenere la prova soltanto gli studenti iscritti; quindi, dopo aver riempito il modulo, seguire il link "torna al modulo" e verificare se la prenotazione è stata effettuata.
  Per cancellare la propria prenotazione, è necessario inviare una email al docente.
  
  Le prenotazioni per la seconda prova devono avvenire tramite il portale dello studente.

LUCIDI utilizzati a lezione.
Attenzione: i lucidi (slides) non sostituiscono le dispense, che si possono invece scaricare da qui.

Alcuni programmi di utilità

Testi di esami

Modalità di esame:

• Per gli studenti dell'ordinamento D.M.270/04 che sostengono l'esame integrale (9 CFU):
  
  
  • l'esame è articolato in due prove, che si svolgeranno separatamente (normalmente, in date diverse).
    La prima prova verterà sugli argomenti 1-3 riportati nel programma del corso, la seconda prova sugli altri argomenti.
  
  
  • Gli studenti che seguono il corso, possono sostenere la prima prova anche nella sessione di esami di Febbraio.
  
  
  • Prenotazioni: Per prenotarsi alla prima prova, gli studenti devono riempire l'apposito modulo, almeno 5 giorni prima della data della prova. Saranno ammessi a sostenere la prova soltanto gli studenti iscritti; quindi, dopo aver riempito il modulo, seguire il link "torna al modulo" e verificare se la prenotazione è stata effettuata. Per cancellare la propria prenotazione, è necessario inviare una email al docente.
    
    Le prenotazioni per la seconda prova devono avvenire tramite il portale dello studente.
  
  
• Gli studenti dell'ordinamento D.M.270/04 che sostengono Logica e Sistemi Informatici come esame integrativo e gli studenti dell'ordinamento D.M.509/99 devono sostenere soltanto la seconda prova. Per i primi sarà eventualmente indicato quali esercizi non dovranno considerare.

• Logic related conferences:
  • http://cm.bell-labs.com/cm/cs/who/libkin/lics/logic-confs.html

  • http://www.dcs.kcl.ac.uk/journals/conferences/conferences.html

• Formal methods: http://archive.comlab.ox.ac.uk/formal-methods.html

• Compulog Net: http://www.cs.reading.ac.uk/archive/compulog.html

• Folli (The European association for Logic, Language and Information): http://www.folli.uva.nl/

• Association for Automated Reasoning (AAR): http://www-unix.mcs.anl.gov/AAR/

• Logic Journal of the IGPL: http://www3.oup.co.uk/igpl/contents/

• J. of AI Research (JAIR): http://www.cs.washington.edu/research/jair/home.html

• Logical Methods in Computer Science (an open-access journal).

• Stanford Enciclopedia of Logic Technology: http://logic.stanford.edu/selt/selt.html

• Dimostrazione automatica
  • Automated Reasoning Systems Database

  • SATLIB - The Satisfiability Library
    SATLIB is a collection of benchmark problems, solvers, and tools for SAT related research.

  • The Logics Workbench LWB
    The Logics Workbench LWB offers the possibility to work in a user-friendly way in classical and non-classical propositional logics, including nonmonotonic approaches.

  • The leanTAP Home Page

  • Automated Reasoning Project della Australian National University

  • Metodi di deduzione per logiche modali (tableaux): si può vedere il Rapporto Tecnico di Rajeev Gore' "Tableau Methods for Modal and Temporal Logic" e la pagina di ModLeanTAP.

  • The Coq proof assistant

• Model Checking:
  • Un articolo di base:

    J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, L. J. Hwang, "Symbolic Model Checking: 10^20 states and beyond", Proceedings. Fifth Annual IEEE Symposium on Logic in Computer Science, Philadelphia, PA, 4-7 June 1990, pp. 428-39.

  • Formal Methods - Model Checking, Carnegie Mellon University, Pittsburg
    Disponibile codice (sistema SMV) e riferimenti a pubblicazioni sul model checking.
  • World Wide Web Virtual Library: Formal Methods
  • Model Checking benchmarks circuits
  • UC Berkeley Design Technology Warehouse
  • Formal Methods Group, Manchester
  • Formal Verification Group, Eindhoven
  • XVGC visualization tool, University of Saarland
  • DaVinci visualization tool, Bremen University