Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
FIŞA DISCIPLINEI

Codul	Disciplina	
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 disciplină	Lect. Dr. LUPEA Mihaiela, lupea@cs.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.
	
Conţinutul	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 &#8211; 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 &#8211; doua sisteme complementare de demonstrare directa 
   - Calculul secventelor - utilizat in verificarea derivabilitatii in logica propozitionala/ predicatelor;
   - Calculul anti-secventelor &#8211; 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 &#8211; metoda de demonstrarea prin respingere
   - Rafinari ale rezolutiei
      &middot;	rezolutia blocarii;
      &middot;	rezolutia liniara (de intrare, unitara, clauze ordonate); metode de cautare in arbori si euristici utilizate in generarea respingerilor liniare;
      &middot;	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%