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 Systems 	

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
- 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)
- To implement ATP (automated theorem prover) systems based on the studied methods.	

IV. Course contents
1. Automated theorem proving systems: architecture, examples, applications.
2. Basic notions of classical logics (propositional logic and first-order logic).
3. Data structures used to represent and manipulate logical formulas.
4. Binary decision diagrams in propositional logic.
5. Semantic tableaux method - a refutation proof method
   - A new approach of semantic tableaux method;
   - Considerations for implementation of an ATP based on this method.
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 based on these methods.
7. Semantic trees 
   - Heuristics and tree-searching methods used to implement an efficient proof 
     procedure based on the construction of semantic trees.
8. Model elimination calculus - a refutation  proof method
   - Connection tableaux used to find a refutation in clausal form 
9. 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)
   Considerations for implementation of ATP systems based on different refinements of 
   resolution.

Laboratory: 
1. Study and work with some dedicated ATP systems.
2. Projects for teams of 3 students: implementation of ATP systems based on the studied 
   methods.

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

VII. Didactic methods used

VIII. Assessment
The final grade is obtained based on:
- written exam: 50%
- laboratory activity: 50%

IX. Additional references

	Dean,							Chair head,

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