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 dintre cele mai active domenii ale inteligentei artificiale, demonstrarea 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.
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. 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.
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. Aplicatii la lingvistica computationala.
5. Domenii de aplicare a demonstrarii automate a teoremelor.
Bibliografie
1."Logic for CS", M.Clarke, ed. Addison Wesley, 1990.
2."First-order logic and Automated Theorems Proving", M.Fitting, Ed .Springer Verlag, 1990.
3. "Logic and Proof", Lawrense C. Paulson, U. Cambridge, 2000, curs on-line.
4."Demonstration Automatique",M.Rusinowitch,ed.Interedition,1989.
5."Bazele matematice ale calculatoarelor",D.Tatar,Reprografia Universitatii "Babes-Bolyai" ,ed. 1993, ed. 2000.
6. "Inteligenta artificiala: demonstrare automata de teoreme si NLP", D.Tatar, Ed. Microinformatica, 2001.
7."From standard logic to Logic Programming", (ed) A.Thayse,ed.J.Wiley, vol1(1989), vol2(1989), vol3(1990).
8.* * *.Turbo Prolog,vol.1 si 2,Borland,1988.
9." Automated Reasoning" L.Woss, Prentice Hall, 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.