Universitatea "Babes-Bolyai" Cluj-Napoca
Facultatea de Matematica si Informatica
FISA DISCIPLINEI

Demonstrare automată şi sisteme de rescriere
Cod
Semes-
trul
Ore: C+S+L
Credite
Tipul
Specializarea
MI020
6
2+1+0
5
optionala
Informatică
MI020
6
2+1+0
4
optionala
Matematică-Informatică
Cadre didactice indrumatoare
Prof. Dr. TATAR Doina,  dtatarcs.ubbcluj.ro
Obiective
Introducerea studentilor in unul dintre cele mai active domenii ale inteligentei artificiale, demonstrarea automata a teoremelor. Parcurgerea tuturor etapelor in implementarea unui demonstrator de teoreme in calculul propozitional si calculul predicatelor. Familiarizarea studentilor cu aplicatiile demonstrarii automate de teoreme in contextul informaticii teoretice si aplicative.
Continut
1. Concepte clasice ale logicii propozitiilor,reguli de transformare a formulelor in forme normale. Utilizarea lor ca domonstrator pentru logica propozitiilor.Metoda rezolutiei,strategii de optimizare.
2. Rezultate clasice in logica predicatelor. Introducerea de domenii pentru termeni si formule in logica predicatelor. Implementarea predicatelor de substitutie si unificare,de aducere la forma Skolem,de eliminarea cuantificatorilor. Implementarea metodei tabelelor semantice ca demonstrator automat de teoreme. Metoda rezolutiei,posibilitati de implementare. Teorii ecuationale. Metoda arborilor semantici.
3. Sisteme de rescriere. Definitii,proprietati de terminare si de confluenta.Sisteme de rescriere si teorii ecuationale. Algoritmul Knuth-Bendix. Demonstrarea teoremelor prin algoritme de completare cu perechi critice.
4. Logici neclasice:logica modala,temporala.
5. Domenii de aplicare a demonstrarii automate a teoremelor.
Bibliografie
1. M. BEN-ARI : Mathematical logic for CS, Ed. Springer, 2001.
2. M. CLARKE : Logic for CS, ed. Addison Wesley, 1990.
3. M. FITTING : First-order logic and Automated Theorems Proving, Ed .Springer Verlag, 1990.
4. L. PAULSON : Logic and Proof, U. Cambridge, 2000, curs on-line.
5. M. RUSINOWITCH : Demonstration Automatique, Ed.Interedition, 1989.
6. J. M. SCHUMANN :Automated Theorem Proving,in Software Engineering, Ed. Springer, 2001.
7. D. TATAR : Bazele matematice ale calculatoarelor, Reprografia Universitatii "Babes-Bolyai" ,ed. 1993, ed. 1999.
8. D. TATAR : Inteligenta artificiala: demonstrare automata de teoreme si NLP, Ed. Albastra, Microinformatica, 2001.
9. * * *.Turbo Prolog, vol.1 si 2,Borland,1988.
10. L. WOS: Automated Reasoning, Prentice Hall, 1993.
Evaluare
Se va evalua gradul de intelegere a materiei predate prin participarea la implementarea demonstratorului de teoreme si dezbaterea la seminarii a unor articole si produse recente, disponibile on-line, din domeniul demonstrarii automate.
Examinarea se face prin examen oral cu subiecte din toata materia predata (70%). Notarea va tine cont si de activitatea de la seminarii (30%).