Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Calculatoare şi tehnologia informaţiei
Programul de studii: Ingineria informatiei - in limba engleza
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MII0006	Automated Theorem Proving 	

Semester	Hours: C+S+L	Category	Status	
6	2+0+2		optional	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
LUPEA Mihaiela	Ph.D.	Lect.	Programming  Languages and Methods	*		*	

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
-  The aim of the course is to study proof methods, which solve specific decisional problems in propositional logic and first-order logic: check if a statement is a theorem or if a statement (the conjecture) is a logical consequence of a set of statements (the axioms and hypotheses).
-  Applications of automated theorem proving in program verification, mathematical reasoning and common-sense reasoning are presented.
-  Automated theorem prover systems based on the studied methods are implemented during the laboratory classes.	

IV. Course contents
1.	Theorem proving methods (binary decision diagrams, semantic tableaux, sequent/anti-sequent calculus, semantic trees, resolution-refinements, clausal-form model elimination) in propositional and first-order logic are studied.
2.	 Based on these methods, considerations for implementing automated theorem proving systems are discussed.
3.    Applications of automated theorem proving in program verification, mathematical reasoning and common-sense reasoning are presented.	

V. 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.	

VI. Thematic of didactic activities per weeks
Lecture 1:  Automated theorem proving (ATP) systems: architecture, examples, applications.

Lecture 2:  Basic notions of classical logics (propositional logic and first-order logic).

Lecture 3:  Data structures used to represent and manipulate logical formulas.

Lecture 4:  Binary decision diagrams in propositional logic.
Lecture 5:  Semantic tableaux method – a refutation proof method
-	 A new approach of semantic tableaux method.
      -     Considerations for implementing an ATP system based on this method.

Lecture 6:  Sequent and anti-sequent  calculi– two complementary direct proof systems
-    Sequent calculus – used to check the derivability in propositional/first-order logic.
-    Anti-sequent calculus- used to check the non-derivability and to build anti-models.
      -    Considerations for implementation of an ATP system based on these methods.

Lectures 7- 9:  Resolution method – a refutation proof method
-	Refinements and strategies of resolution
•	lock resolution
•	linear resolution (input, unit, ordered); 
•	semantic resolution (hyper-resolution, the set-of support-strategy, ordered)
-	Heuristics and tree-searching methods used in implementation.

Lecture 10:   Semantic trees 
-	Heuristics and tree-searching methods used to implement an efficient proof procedure based on
       the construction of semantic trees.

Lecture 11:   Model elimination calculus – a refutation  proof method
-	Connection tableaux used to find a refutation in clausal-form model elimination  procedure.

Lectures 12 - 13:
    Applications of automated theorem proving in program verification, mathematical reasoning (algebra, geometry) and common-sense reasoning (knowledge bases).  

Week 14:  Written exam.
Laboratory classes:
Weeks 1-3: Study and work with some dedicated ATP systems based on sequent calculus, tableaux,                           model elimination or resolution:  3TAP, ft, Gandalf, LeanTAP, METEOR, Otter, Prover9, SATURATE, SETHEO and Vampire.
Weeks 4-13: Software projects for teams of 3 students: implementation of ATP systems based on the 
                    studied methods.
Week 14: Projects’ evaluation.	

VII. Didactic methods used
    Expositions: description, explanation, class lectures, dialog-based lectures, lectures with demonstrations, introductive lectures, current lectures, synthesis lectures. 
   Conversations: debate, dialog, introductive conversations, conversations for knowledge consolidation, conversations to systematize and synthesize knowledge. 
   Use of problems: use of problem questions, problems and problem situations. 
  Other methods: case study; cooperation, simulation, brainstorming, individual study, exercise, homework study.	

VIII. Assessment
The activity ends with a written final exam. During the laboratory classes, teams of 2-3 students have to implement an ATP system.  The final grade is obtained based on:
  - written exam: 50%
  - laboratory activity (software project): 50%
 Successful passing of the exam is conditioned by the written exam’s grade to be at least 5.
 All university official rules with respect to students’ attendance of academic activities, as well as to cheating and plagiarism, are valid and enforced.

http://cs.ubbcluj.ro/~lupea/Optional_Automated_Proof_Systems

IX. Additional references
1.W.Bibel: Automated theorem proving, View Verlag, 1987.
2.M.Lupea: Theorem proving in classical logics, electronic format, Cluj-Napoca, 2008.
3. (ed) A.Thayse: From standard logic to Logic Programming, Ed. J.Wiley, vol1(1989), vol2(1989), vol3(1990).
http://www.cs.otago.ac.nz/staffpriv/hans/logiccourseware.html
http://www-formal.stanford.edu/clt/ARS/systems.html	

	Date,							Course responsible,
       26.11.2008                        				Lect. LUPEA Mihaiela, Ph.D.