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

FISA DISCIPLINEI

Codul
Denumirea disciplinei
MII0006 Sisteme de demonstrare automata
Specializarea
Semestrul
Ore: C+S+L
Categoria
Statutul
Informatică - în limba engleză
4
2+0+2
specialitate
optionala
Ingineria informatiei - in limba engleza
6
2+0+2
optionala
Ingineria informatiei - in limba engleza
8
2+0+2
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. Metoda conectiei
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