Logica e Sistemi Informatici

Avvisi:

• Orario di ricevimento studenti durante il secondo periodo didattico: giovedì, ore 10 (escluso il periodo dal 24 dicembre al 6 gennaio).
• Risultati dell'ultima prova scritta: Febbraio 2010 (Prima parte).
  Giovedì 18 febbraio alle ore 11 sarà possibile avere visione dei compiti.
  
  

LUCIDI utilizzati a lezione

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 parti, che si svolgeranno separatamente.
  La prima parte verterà sugli argomenti 1-3 riportati nel programma del corso, la seconda parte sugli altri argomenti.
  Nell'interruzione didattica di febbraio è prevista una prova intermedia corrispondente alla prima parte dell'esame.
  Nel caso in cui non sia possibile prenotarsi per la prova intermedia o la prima parte dell'esame sul portale dello studente, gli studenti che intendono sostenerla devono prenotarsi inviando una mail al docente almeno una settimana prima della data dell'appello.
  
• 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 parte dell'esame. 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