Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat

FISA DISCIPLINEI

Codul
Denumirea disciplinei
MII1003 Sisteme de demonstrare automată
Specializarea
Semestrul
Ore: C+S+L
Categoria
Statutul
Metode formale în programare - în limba engleză
3
2+1+1
specialitate
obligatorie
Titularii de disciplina
Lect. Dr. LUPEA Mihaiela,  lupeacs.ubbcluj.ro
Obiective
- Studierea metodelor de demonstrare, specifice logicilor clasice şi logicilor temporale, pentru rezolvarea problemei decizionale: "Este o afirmaţie dată o consecinţă logică a unei mulţimi de axiome şi ipoteze?".
- Aplicarea metodelor de demonstrare în specificarea şi verificarea programelor secvenţiale şi a programelor concurente.
- Implementarea unor sisteme de demonstrare automată pentru logicile clasice şi logicile temporale.
Continutul
1. Demonstrarea automată: scop, aplicaţii, exemple de sisteme de demonstrare automată.
2. Metode de demonstrare în logica propoziţiilor: tabele semantice, calculul
secvenţelor / calculul anti-secvenţelor, rafinări ale rezoluţiei.
3. Metode de demonstrare automată în logica predicatelor: tabele semantice, calculul
secvenţelor / calculul anti-secvenţelor, rafinări ale rezoluţiei.
4. Demonstrarea automată şi programarea logică: rezoluţia SLD, programarea logică
concurentă.
5. Logici propoziţionale temporale: liniare, ramificate; semantica: automate Buchi.
6. Metode de demonstrare în logicile temporale: tabele semantice şi rezoluţie.
7. Specificarea şi verificarea programelor concurente utilizând logicile temporale.
Bibliografie
1. C.L.Chang, R.C.T.Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press,
1973.
2. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in
Computer Science, Springer Verlag, 1990, Second Edition 1996.
3. M.R. Genesereth, N.J. Nilsson: Logical Foundations of Artificial Intelligence, Morgan
Kaufman, 1992.
4. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991.
5. L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
6. M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line.
7. S.Reeves, M.Clarke: Logic for computer science, Addison Wesley Publisher Ltd, 1990.
8. N.Rescher, A.Urquhart: Temporal Logic, Springer Verlag, New York, 1971.
9. R.M.Smullyan: First-order logic, Revised Edition, Dover Press, New York, 1996.
10. D.Tatar: Inteligenta artificiala: demonstrarea automata si NLP, Editura
Microinformatica, Cluj-Napoca, 2001.
Evaluare
Activitatea se încheie cu un examen final scris.
Pe parcursul semestrului studenţii trebuie să pregătească şi să prezinte în timpul seminariilor 11-12-13 un referat teoretic cu subiect din domeniul demonstrării automate.
Un proiect soft, constând în implementarea unui sistem de demonstrare automată în logicile clasice sau temporale, va fi realizat individual de către fiecare student şi va fi prezentat în timpul ultimei săptămâni a semestrului.
Nota finală se obţine astfel:
- examen scris: 40%
- activitate seminarii: 10%
- referat teoretic: 25%
- proiect soft: 25%
Pentru promovare, nota de la examenul scris trebuie să fie minimum 5.
Sunt valabile regulamentele oficiale ale universităţii în legătură cu prezenţa studenţilor la activităţile didactice, cazurile de copiat şi plagiat.
Legaturi: Syllabus-urile tuturor disciplinelor
Versiunea in limba engleza a acestei discipline
Versiunea in format rtf a acestei discipline