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

FISA DISCIPLINEI

Codul
Denumirea disciplinei
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 disciplina
Lect. Dr. LUPEA Mihaiela,  lupeacs.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.

Continutul
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%
Legaturi: Syllabus-urile tuturor disciplinelor
Versiunea in limba engleza a acestei discipline
Versiunea in format rtf a acestei discipline