"Babes-Bolyai" University of Cluj-Napoca
Faculty of Mathematics and Computer Science
| 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. 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. |
| 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%). |