Subject: Automated Theorem Proving and Term Rewriting Systems	Code: MI020	

Semester	 Hours: C+S+L	Type	 Section	
6	2+1+0	optional	Computer Science	
6	2+1+0	optional	Mathematics-Computer Science	

Teaching Staff in Charge	Prof. TATAR Doina, Ph.D., dtatar@cs.ubbcluj.ro
Lect. LUPEA Mihaiela, Ph.D., lupea@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. Semantic tree method. 
2. Rewriting systems as tools in automated theorem proving. Knuth-Bendix algorithm and completion with critical pairs. 
3.  Theorem proving in nonstandard logics.
4.  Some fields of applications for automated theorem proving: circuits verification, computational linguistics	
Selective References	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.	
Assessment	The examination consists of oral exam with the subjects from all the matter (70%).
Presentation during of the seminars of  some recent papers and on-line software  in automated theorem proving will be also evaluated (30%)