Babes-Bolyai University of Cluj-Napoca
Faculty of Mathematics and Computer Science
Study Cycle: Master
SUBJECT

Code	Subject	
MI369	Automated Theorem Proving	

Section	Semester	Hours: C+S+L	Category	Type	
Formals Methods in Programming - in English	2	2+2+1		compulsory	

Teaching Staff in Charge	Lect. LUPEA Mihaiela, Ph.D., lupea@cs.ubbcluj.ro	
Aims	- To study proof methods, specific to propositional and first-order logics, which solve 
  the decision problems: check if a statement is a theorem or if a statement is a   
  logical consequence of a set of axioms and hypotheses;
- To implement ATP (automated theorem prover) systems based on the studied methods.
- To apply the ATP systems for programs specification and verification.
	
Content	1. Basic notions of classical logics (propositional logic and first-order logic)
2. Formalization of common-sense reasoning and mathematical reasoning using these 
   classical logics. 
3. Semantic tableaux method - a refutation proof method
     - A new approach of semantic tableaux method;
     - Considerations for implementation of an ATP based on this method, which solves the
        following decision problems:
           - build all the models of a consistent formula
           - check if a formula is a tautology
           - check if a formula is a logical consequence of a set of axioms and 
              hypotheses;
4.Sequent and antisequent  calculi- two complementary direct proof systems
     - Sequent calculus - used to check the derivability in propositional/first-order 
       logic
     - Antisequent calculus- used to check the non-derivability and to build anti-models
     - Considerations for implementation of an ATP based on these methods;
5. Theorem prover based on semantic trees and Herbrand Theorem 
     - Heuristics and tree-searching methods used to implement an efficient proof 
       procedure based on the construction of semantic trees
6. Model elimination calculus - a refutation  proof method
     - Connection tableaux used to find a refutation in clausal-form model elimination  
        procedure
7. Resolution method - a refutation proof method
     -	Refinements of resolution
       -  lock resolution
       -  linear resolution (input, unit, ordered); tree-searching methods and heuristics
          used to find linear refutations;
       -  semantic resolution (hyperresolution, the set-of support-strategy,ordered)
     - Considerations for implementation of  ATP systems based on different refinements 
       of resolution.
8. Applications of theorem proving in programs specification and verification.
	
Bibliography	1. M. Ben-Ari: Mathematical Logic for Computer Science, Ed. Springer, 2001. 
2. C.L.Chang, R.C.T.Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 
   1973.
3. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in 
   Computer Science, Springer Verlag, 1990, Second Edition 1996.
4. M.R. Genesereth, N.J. Nilsson: Logical Foundations of Artificial Intelligence, Morgan 
   Kaufman, 1992.
5. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991.
6. L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
7. M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line.
8. S.Reeves, M.Clarke: Logic for computer science, Addison Wesley Publisher Ltd, 1990.
9. D.Tatar: Inteligenta artificiala: demonstrarea automata si NLP, Editura 
   Microinformatica, Cluj-Napoca, 2001.
10. R.M.Smullyan: First-order logic, Revised Edition, Dover Press, New York, 1996.
	
Assessment	The final grade is obtained based on:
- written exam: 40%
- seminar activity: 10%
- presentation of a theoretical paper: 25%
- individual project- implementation of an ATP system: 25%