Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
FISA DISCIPLINEI
| MII1003 | Sisteme de demonstrare automată |
| Titularii de disciplina |
Lect. Dr. LUPEA Mihaiela, lupea cs.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. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991. 3. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer Verlag, 1990, Second Edition 1996. 4. M.Lupea, A.Mihis: Logici clasice si circuite logice. Teorie si exemple, Ed.Albastra, editia 2, 2009. 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 |