Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Informatică
Programul de studii: Informatică - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MII0006	Automated Theorem Proving 	
		
Semester	Hours: C+S+L	Category	Status	
4	2+0+1	speciality	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	*		*	

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.	M. Lupea, A. Mihis: Logici clasice şi circuite logice. Teorie şi exemple, ediţia 2, Editura Albastra,
      Cluj-Napoca, 2009 - bibliotecă.
7.	L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
8.	M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line.
9.	S.Reeves, M.Clarke: Logic for computer science, Addison Wesley Publisher Ltd, 1990.
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.

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

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

Lectures 9- 11:
     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.

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 , Vampire, PC Prove, etc.
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 3 students have to implement an ATP system.  The final grade is obtained based on:
  - written exam: 50%
  - laboratory activity: 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. 	

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. D.Tatar: Inteligenta artificiala: demonstrarea automata si NLP, Editura Microinformatica, 
    Cluj- Napoca, 2001.
4. (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,
          1.10.2009          					Lect. LUPEA Mihaiela, Ph.D.