Babes-Bolyai University of Cluj-Napoca
Faculty of Mathematics and Computer Science
Study Cycle: Graduate
SUBJECT
| MII0020 | Automated Theorem Proving |
| Teaching Staff in Charge |
Lect. LUPEA Mihaiela, Ph.D., lupea cs.ubbcluj.ro |
| Aims |
|
- 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. |
| Content |
|
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. |
| References |
|
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. D.A. Duffy: Principles of automated theorem proving, John Willey & Sons, 1991. 4. M.Fitting: First-order Logic and Automated Theorem Proving, Texts and Monographs in Computer Science, Springer Verlag, 1990, Second Edition 1996. 5. M.R. Genesereth, N.J. Nilsson: Logical Foundations of Artificial Intelligence, Morgan Kaufman, 1992. 6. M.Lupea, A.Mihis: Logici clasice si circuite logice. Teorie si exemple, Ed.Albastra, editia 2, 2009. 7. L.C. Paulson: Logic and Proof, Univ. Cambridge, 2000, course on-line. 8. M. Possega: Deduction Systems, Institute of Informatics, 2002, course on-line. 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 final grade is obtained based on:
- written exam: 50% - laboratory activity: 50% |
| Links: | Syllabus for all subjects Romanian version for this subject Rtf format for this subject |