Babes-Bolyai University of Cluj-Napoca
Faculty of Mathematics and Computer Science
Study Cycle: Master
SUBJECT
| MII1003 | Automated Theorem Proving Systems |
| Teaching Staff in Charge |
Lect. LUPEA Mihaiela, Ph.D., lupea cs.ubbcluj.ro |
| Aims |
|
- 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. |
| Content |
|
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. |
| References |
|
1. C.L.Chang, R.C.T.Lee: Symbolic Logic and Mechanical Theorem Proving, Academic Press,
1973. 2. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991. 3. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer Verlag, 1990, Second Edition 1996. 4. M.Lupea, A.Mihis: Logici clasice si circuite logice. Teorie si exemple, Ed.Albastra, editia 2, 2009. 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. |
| 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. |
| Links: | Syllabus for all subjects Romanian version for this subject Rtf format for this subject |