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

FISA DISCIPLINEI

Codul
Denumirea disciplinei
MII0006 Sisteme de demonstrare automată
Specializarea
Semestrul
Ore: C+S+L
Categoria
Statutul
Informatică - în limba engleză
4
2+0+2
specialitate
optionala
Informatică - în limba engleză
6
2+0+2
specialitate
optionala
Titularii de disciplina
Lect. Dr. LUPEA Mihaiela,  lupeacs.ubbcluj.ro
Obiective
- Cunosterea unor metode de demonstrare în logica propozitiilor si logica predicatelor pentru rezolvarea problemelor decizionale: verificarea dacă o afirmaţie este teoremă sau este o consecinţă logică a unei mulţimi de axiome şi ipoteze;
- Implementarea unor sisteme de demonstrare automată bazate pe metodele studiate.
Continutul
1. Sisteme de demonstrare automata: scop, arhitectura, exemple, aplicatii.
2. Notiuni de bază in logicile clasice (logica propozitiilor si logica predicatelor de ordinul I)
3.Structuri de date utilizate in reprezentarea si manipularea formulelor logice.
4 Diagrame binare de decizie in logica propozitiilor.
5 Metoda tabelelor semantice – metoda de demonstrare prin respingere
- O noua versiune a metodei tabelelor semantice
- Consideratii de implementare a unui sistem de demonstrare automată
6. Calculul secventelor si calculul anti-secventelor – doua sisteme complementare de demonstrare directa
- Calculul secventelor - utilizat in verificarea derivabilitatii in logica propozitionala/ predicatelor;
- Calculul anti-secventelor – utilizat in verificarea nederivabilitatii si construirea antimodelelor;
- Consideratii de implementare a sistemelor de demonstrare automata bazate calculul secventelor si calculul anti-secventelor.
7. Demonstrator automat bazat pe arbori semantici
- Euristici si metode de cautare in arbori, utilizate in implementarea unei proceduri eficiente de construire a arborilor semantici.
8. Eliminarea modelelor in forma clauzala- metoda de demonstrare prin respingere
- Tabele de conexiune utilizate in generarea respingerii folosing calculul eliminarii modelelor
9. Metoda rezolutiei – metoda de demonstrarea prin respingere
- Rafinari ale rezolutiei
· rezolutia blocarii;
· rezolutia liniara (de intrare, unitara, clauze ordonate); metode de cautare in arbori si euristici utilizate in generarea respingerilor liniare;
· rezolutia semantica (hyper-rezolutia, strategia multimii suport, clauze ordonate).
- Consideratii de implementare a sistemelor de demonstrare automata bazate pe rafinarile rezolutiei

Laborator:
1. Studierea si utilizarea unor sisteme de demonstrare automata existente.
2. Proiecte pentru echipe de 3 studenti: implementarea de sisteme de demonstrare automata bazate pe metodele studiate.
Bibliografie
1. M. Ben-Ari: Mathematical Logic for Computer Science, Ed. Springer, 2001.
2. C.L.Chang, R.C.T.Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
3. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer Verlag, 1990, Second Edition 1996.
4. M.R. Genesereth, N.J. Nilsson: Logical Foundations of Artificial Intelligence, Morgan Kaufman, 1992.
5. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991.
6. L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
7. M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line.
8. S.Reeves, M.Clarke: Logic for computer science, Addison Wesley Publisher Ltd, 1990.
9. D.Tatar: Inteligenta artificiala: demonstrarea automata si NLP, Editura Microinformatica, Cluj-Napoca, 2001.
10. R.M.Smullyan: First-order logic, Revised Edition, Dover Press, New York, 1996.

Evaluare
Notata finală este obtinută din:
- examen scris: 50%
- activitate laborator: 50%
Legaturi: Syllabus-urile tuturor disciplinelor
Versiunea in limba engleza a acestei discipline
Versiunea in format rtf a acestei discipline