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	
3	2+1+1	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 
   calculus/anti-sequent calculus, refinements of resolution.
3. Theorem proving methods in predicate logic: semantic tableaux, 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
7. 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. L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line.
6. M. Possega: Deduction Systems, Institute of Informatics, 2002, 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

VII. Didactic methods used

VIII. Assessment
 The activity ends with a written final exam. 
 During the semester, the students have to prepare and to present at seminars 11-12-13 a theoretical report with the subject from 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

	Dean,							Chair head,

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