Universitatea "Babeş-Bolyai" din Cluj-Napoca

Facultatea de Matematică şi Informatică
FISA DISCIPLINEI

Demonstrare automată şi sisteme de rescriere

Automated theorem proving and term rewriting systems

Cod	Semes- trul	Ore: C+S+L	Credite	Tipul	Sectia
MI020	4	2+1+0	5	optionala	Tehnologie Informatică (College of Computer Technology)
MI020	6	2+1+0	5	optionala	Informatică (Computer Science)

Cadre didactice indrumatoare

Teaching Staff in Charge

Conf. Dr. TĂTAR Doina, dtatar@cs.ubbcluj.ro

Obiective	Aims
Introducerea studentilor in unul dun cele mai active domenii ale informaticii, demonstrarea teoremelor. Parcurgerea tuturor etapelor in implementarea unui demonstrator de teoreme. Familiarizarea studentilor cu legaturile acestui domeniu in contextul informaticii teoretice si aplicative.	The aims of the course is the presentation of one of the most active domains in artificial intelligence, automated theorem proving. There are presented the stages for implementations of an automated prover. The aplications of this domain in others fields of computer science are surveyed.

Continut

1. Elemente de demonstrare automata a teoremelor. Transformarea formulelor din logica propozitiilor in forme normale.Implementarea acestor transformari. Utilizarea sa ca demonstrator pentru logica propozitiilor. Metoda rezolutiei, strategii de optimizare, metode de implementare. Rezultate clasice in logica predicatelor. Introducerea de domenii pentru termeni si formule. Implementarea predicatelor de substitutie si unificare, de aducere la forma Skolem, de eliminarea cuantificatorilor. Implementarea metodei tabelelor semantice ca demonstrator automat de teoreme. Teorii ecuationale. 2. Sisteme de rescriere in demonstrarea automata. Definitii ale sistemelor de rescriere,proprietati de terminare si de confluenta. Sisteme de rescriere si teorii ecuationale. Algoritmul Knuth-Bendix. Implementarea algoritmului. Demonstrarea teoremelor prin algoritme de completare cu perechi critice. 3. Semantici ale programarii,cu aplicatii la programarea logica. Semantica declarativa,procedurala si semantica negatiei. Semantica operationala si denotationala: echivalenta diferitelor formalisme. 4. Abordarea din punct de vedere al limbajelor formale a sistemelor de rescriere si a programarii logice. Arbori de demonstratie, caracterizarea ecuationala a arborilor. Gramatici clauzale si gramatici cu atribute relationale, functionale, conditionale. Legatura lor cu programele logice si sistemele de rescriere.

Bibliografie

1. "Deduction systems in A.I.", ed.K.H.Blasius, H.J.Burkert, 1989. 2. "A grammatical view of Logic Programming" ,P.Deransart, J.Maluszynski, ed.MIT, 1993. 3. "First-order logic and Automated Theorems Proving" M.Fitting, ed. Springer Verlag, 1990. 4. "Theoretical foundations of Computer Science", Dino Mandrioli, Carlo Geizzi, ed.J.Wiley, 1987. 5. "Deductive databases and logic programming", Subrata Kumar Das, ed. Addison-Wesley, 1992. 6. "Bazele matematice ale calculatoarelor", D.Tatar, Tipografia Universitatii "Babes-Bolyai", 1993. 7. "From standard logic to Logic Programming", A.Thayse, ed.J.Wiley, vol1 (1989),vol2 (1989),vol3 (1990). 8. "Artificial Intelligence Programming with Turbo Prolog", K.Weiskamp, T.Hengl, ed.John Willey, 1988. 9. * * * Turbo Prolog, vol.1 si 2, Borland, 1988. 10." Automated Reasoning" L.Woss, Prentice Hall, 1993. 11. "Deduction. Automated logic", W.Bibel ,Academic Press, 1993.

Evaluare	Assessment
Gradul de intelegere a materiei predate Participarea la implementarea demonstratorului de teoreme Interesul pentru aplicarea cunostintelor obtinute Examinarea se face prin examen oral cu subiecte din toata materia predata.	The examination consists of oral exam with the subjects from all the matter.