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

Codul	Disciplina	
MI369	Demonstrare automata	

Specializarea	Semestrul	Ore: C+S+L	Categoria	Statutul	
Metode formale în programare - în limba engleză	2	2+2+1		obligatorie	

Titularii de disciplină	Lect. Dr. LUPEA Mihaiela, lupea@cs.ubbcluj.ro	
Obiective	- Studierea 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; 
- Utilizarea sistemelor de demonstrare automată în specificarea şi verificarea 
  programelor.

Conţinutul	1. Notiuni de bază in logicile clasice (logica propozitiilor si logica predicatelor de 
   ordinul I)
2. Modelarea rationamentului matematic si a celui cotidian valid folosind logicile 
   clasice
3. Metoda tabelelor semantice - metoda de demonstrare prin respingere
    - O noua versiune a metodei tabelelor semantice
    - Consideratii de implementare a unui sistem de demonstrare automată care rezolva 
       urmatoarele probleme decizionale:
      -	Construirea modelelor unei formule consistente
      -	Verificarea daca o formula este tautologie
      -	Verificarea dacă o formula este consecinta logica a unei multimi de formule
4. 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.
5. Demonstrator automat bazat pe arbori semantici si teorema lui Herbrand 
      -	Euristici si metode de cautare in arbori, utilizate in implementarea unei 
       proceduri eficiente de construire a arborilor semantici.
6. Eliminarea modelelor in forma clauzala- metoda de demonstrare prin respingere
   - Tabele de conexiune utilizate in generarea respingerii  folosind calculul eliminarii
     modelelor.
7. 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.
8.Aplicatii ale demonstrarii automate in specificarea si verificarea programelor.	
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: 40%
- activitate seminar: 10%
- referat teoretic: 25%
- proiect individual- implementarea unui demonstrator automat: 25%