Study form: Fulltime
Course language: English
This course will explain the theoretical principles underlying systems for automated theorem proving (model-checking, resolution, tableaux) and the practical and theoretical limitations of these systems. Furthermore, attention will be paid to programming in the language Prolog, in which a formal-proof strategy provides a mechanism for symbolic computation.
1. Formulating, representing and solving problems in the Boolean domain. Soundness and completeness of deductive logical systems.
2. The DPLL method, its implementation and practical applications.
3. Model-checking as a tool for verification. Applications in finite automata.
4. Automated proving in general domains. Problem formulation and representation in predicate logic.
5. The workflow of resolution provers. Conversion to clauses. The ANL loop.
6. Tableaux proving methods; proving with equality; conversion to DPLL.
7. Model finding methods and systems for general domains.
8. Practical and theoretical limits of existing methods and systems; their algorithmic complexity.
9. Programming as proving; the Prolog language, facts, rules, queries, functors, list operations.
10. Definite clauses; the closed-world assumption; decidability in Prolog.
11. Cut, negation, extra-logical operators, meta-interpreters
12. Inductive reasoning in Prolog
13. Definite clause grammars, natural language processing in Prolog
14. Constraint logic programming
Bundy, A.: The Computational Modelling of Mathematical Reasoning, Academic Press 1983 (Bundy).
Clarke, E.M. Jr., Grumberg, O. and Peled, D. A.: Model Checking, The MIT Press, 1999, Fourth Printing 2002.
Newborn, M.: Automated Theorem Proving: Theory and Practice
Robinson, J.A., Voronkov, A. (Eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press 2001
Weidenbach, Ch.: SPASS: Combining Superposition, Sorts and Splitting (1999)
Wos, L. and Pieper, G.W.: A Fascinating Country in the World of Computing: Your Guide to Automated Reasoning
Flach P.: Simply Logical ? Intelligent Reasoning by Example, John Wiley, 1998
Bratko I.: Prolog Programming for Artificial Intelligence, Addison-Wesley, 2011