Automated theorem proving and term rewriting systems 
ter 

Teaching Staff in Charge 

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. KnuthBendix 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. 
References 
1. M. BENARI : Mathematical logic for CS, Ed. Springer, 2001.
2. M. CLARKE : Logic for CS, ed. Addison Wesley, 1990. 3. M. FITTING : Firstorder logic and Automated Theorems Proving, Ed .Springer Verlag, 1990. 4. L. PAULSON : Logic and Proof, U. Cambridge, 2000, curs online. 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 "BabesBolyai" ,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 online software in automated theorem proving will be also evaluated (30%). 