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

Codul	Disciplina	
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 disciplină	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.
	
Conţinutul	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.