"Babes-Bolyai" University of Cluj-Napoca
Faculty of Mathematics and Computer Science

Automated theorem proving and term rewriting systems
Code
Semes-
ter
Hours: C+S+L
Credits
Type
Section
MI020
6
2+1+0
5
optional
Informatică
MI020
6
2+1+0
4
optional
Matematică-Informatică
Teaching Staff in Charge
Assoc.Prof. TATAR Doina, Ph.D., dtatar@cs.ubbcluj.ro
Aims
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.
Content
1. The normal forms as the first step in theorem proving. Tableaux method and resolution method in first order logic: implementation of substitution, unification, and Skolem normal forms.
2. Rewriting systems as tools in automated theorem proving. Knut-Bendix algorithm and completion with critical pairs.
3. Thorem proving in nonstandard logics.
4. Some fields of applications for automated theorem proving: circuits verification, computational linguistics.
References
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. 1999.
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.
Assessment
The examination consists of oral exam with the subjects from all the matter.