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	
MII0020	Automated Theorem Proving	

Semester	Hours: C+S+L+P	Category	Status	
4	2+0+1+1	complementary	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.	Computer Science	*		*	

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)
  Automated theorem prover systems based on the studied methods are implemented during the laboratory and project 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 and heuristics are discussed.
3.    Applications of automated theorem proving in mathematical reasoning, programs’ verification 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 3, Editura Albastra,
      Cluj-Napoca, 2011.
7.	L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
8.	S.Reeves, M.Clarke: Logic for computer science, Addison Wesley Publisher Ltd, 1990.
9.  R.M.Smullyan: First-order logic, Revised Edition, Dover Press, New York, 1996.
10. D.Tatar: Inteligenta artificiala: demonstrarea automata si NLP, Editura Microinformatica, 
     Cluj-Napoca, 2001.	

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, which solves the following 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;

Lectures 6- 8:   Resolution method – a refutation proof method
-	Refinements 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 9:  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 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 programs’ verification, mathematical reasoning (algebra, geometry) and common-sense reasoning (knowledge bases).  

Week 14:  Written exam.

Laboratory classes:
Weeks 1/2,3/4: 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, PCProve, Jape, etc.

Weeks 5/6, 7/8, 9/10,11/12: Software projects for teams of 2 students: implementation of ATP systems based on the studied methods.

Week 13/14: Projects’ evaluation.

Semester Project:
A collective project with an appropriate interface will incorporate all the teams’ projects and will be used as an educational tool for theorem proving in mathematics and programs’ verification.

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 students have to implement an ATP system. A collective project will incorporate all the teams’ projects.

 The final grade is obtained based on:
  - written exam: 50%
  - laboratory + project 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, 2008. 
3. M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line.
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	

	Dean,							Chair head,
	Prof. dr. TAMBULEA Leon			Prof. Dr.  BOIAN Florian Mircea

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