Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
Domeniul: Informatica
Programul de studii: Metode formale în programare - în limba engleză
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MII1003	Automated Theorem Proving Systems	

Semester	Hours: C+S+L	Category	Status	
2	2+1+0	speciality	compulsory	

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
•	To study proof methods, specific to classical logics and temporal logics which solve the decision problem: “Is a conjecture a logical consequence of a set of axioms and hypotheses?”.
•	To apply the theorem proving methods for specification and verification of sequential and concurrent programs.
•	To implement ATP (automated theorem prover) systems in classical logics and temporal logics based on the studied methods.	

IV. Course contents
1. Automated theorem proving:  purpose, applications, examples of ATP systems.
2. Theorem proving methods in propositional logic: semantic tableaux, sequent/anti-sequent calculus, 
    refinements of resolution.
3. Theorem proving methods in predicate logic: semantic tableaux, sequent alculus, refinements of resolution.
4. Theorem proving and logic programming: SLD-resolution; concurrent logic programming.
5. Temporal logics
•	Propositional temporal logic: syntax, semantics, models of time.
•	From temporal logic to finite and Buchi automata.
•	Linear-time and branching-time temporal logics
6. Theorem proving methods in temporal logic
•	Semantic tableaux method for propositional temporal logic
•	Resolution method for linear propositional temporal logic
8. Specification and verification of concurrent programs using temporal logics. 	

V. Bibliography
1. C.L.Chang, R.C.T.Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press, 1973.
2. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer Verlag, 1990, Second Edition 1996.
3. M.R. Genesereth, N.J. Nilsson: Logical Foundations of Artificial Intelligence, Morgan Kaufman, 1992.
4. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991.
5. M. Lupea, A. Mihis: Logici clasice şi circuite logice. Teorie şi exemple, ediţia 2, Editura Albastra,
      Cluj-Napoca, 2009.
6. L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
7. S.Reeves, M.Clarke: Logic for computer science, Addison Wesley Publisher Ltd, 1990.
8. N.Rescher, A.Urquhart: Temporal Logic, Springer Verlag, New York, 1971.
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
Week 1: Lecture1 + Seminar 1:
       Automated theorem proving:  purpose, applications, examples of ATP systems.

Week 2: Lecture 2 + Seminar 2: 
      Theorem proving methods in propositional logic (part I)
•	Binary decision diagrams 
•	A new approach of semantic tableaux method; considerations for implementation.

Week 3: Lecture 3+ Seminar 3:
      Theorem proving methods in propositional logic (part II)
•	Sequent calculus and anti-sequent calculus; considerations for implementation. 

Week 4: Lecture 4 + Seminar 4: 
      Theorem proving methods in propositional logic (part III)
•	Resolution method- refinements (semantic resolution, linear ordered resolution)
•	Heuristics used in implementation.

Week 5: Lecture 5 + Seminar 5: 
      Theorem proving methods in predicate logic (part I)
•	A new approach of semantic tableaux method
•	Sequent calculus and anti-sequent calculus
•	Considerations for implementing ATP systems based on these methods.

Week 6: Lecture 6+ Seminar 6: 
      Theorem proving methods in predicate logic (part II)
•	Semantic resolution method –  considerations for implementation.

Week 7: Lecture 7+ Seminar 7: 
      Theorem proving methods in predicate logic (part III)
•	Linear ordered resolution method –  considerations for implementation.

Week 8: Lecture 8+ Seminar 8:
      Theorem proving and logic programming
•	SLD-resolution; soundness and completeness.
•	Concurrent logic programming.

Week 9: Lecture 9 + Seminar 9:
       Propositional temporal logic: syntax, semantics, models of time.
•	From temporal logic to finite and Buchi automata.
•	Linear-time temporal logic and branching-time temporal logic

Week 10: Lecture 10+ Seminar 10: 
       Theorem proving methods in temporal logic (part I)
•	Semantic tableaux method for propositional temporal logic
•	Model checking using semantic tableaux in linear-time and branching-time temporal logic

Week 11: Lecture 11 + Seminar 11:
        Theorem proving methods in temporal logic (part II)
•	Resolution method for linear propositional temporal logic

Week 12: 
       Lecture 12: Program verification using resolution in predicate logic. 
       Seminar 12: Students’ presentations of theoretical reports.

Week 13: 
       Lecture 13: Specification and verification of concurrent programs using temporal logics.
       Seminar 13: Students’ presentations of theoretical reports. 

Week 14: 
       Evaluation of practical projects. 

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. 
     discovery, discovery by documenting, experimental discovery. 
Other methods: case study; cooperation, simulation, individual study, exercise, homework study.	

VIII. Assessment
The activity ends with a written final exam. 
During the semester, the students will have to prepare and to present at seminars 11-12-13 a theoretical report with the subject from the theorem proving domain.
An individual software project: implementation of an ATP system for classical logics or temporal logics must be accomplished. 
 The final grade is obtained based on:
     - written exam: 40%
     - seminar activity: 10%
     - theoretical report: 25%
     - software project: 25%
  Successful passing of the exam is conditioned by 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. M. Ben-Ari: Mathematical Logic for Computer Science, Ed. Springer, 2001. 
2. W. Bibel: Automated theorem proving, View Verlag, 1987.
3. M. Lupea: Automated theorem proving in classical logics, electronic format, Cluj-Napoca, 2006.
4. M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line.
5. (ed) A.Thayse: From standard logic to Logic Programming, Ed. J.Wiley, vol1(1989), vol2(1989), vol3(1990).	

	Date,							Course responsible,

       1.10.2009						      Lect. LUPEA Mihaiela, Ph.D.