Universitatea "Babes-Bolyai" Cluj-Napoca
Facultatea de Matematica si Informatica
FISA DISCIPLINEI
| Demonstrare automata |
trul |
||||
| Cadre didactice indrumatoare |
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; - Utilizarea sistemelor de demonstrare automată în specificarea şi verificarea programelor. |
| Continut |
|
1. Notiuni de bază in logicile clasice (logica prpropozitiilor 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 |