IA085 Satisfiability and Automated Reasoning

Faculty of Informatics
Spring 2024
Extent and Intensity
2/1/1. 4 credit(s) (plus extra credits for completion). Type of Completion: zk (examination).
Taught in person.
Teacher(s)
RNDr. Martin Jonáš, Ph.D. (lecturer)
Bc. Jakub Šárník (seminar tutor)
Guaranteed by
RNDr. Martin Jonáš, Ph.D.
Department of Computer Science – Faculty of Informatics
Supplier department: Department of Computer Science – Faculty of Informatics
Timetable
Wed 16:00–17:50 A217
  • Timetable of Seminar Groups:
IA085/01: each odd Monday 10:00–11:50 B204, J. Šárník
Course Enrolment Limitations
The course is offered to students of any study field.
Course objectives
At the end of the course, students should:
- have working knowledge of propositional logic and first-order logic,
- be able to express real-world problems in a suitable logical formalism,
- be able to explain principles, algorithms, and underlying theoretical concepts of modern satisfiability solvers and theorem provers,
- be able to assess what kind of tool is relevant for their problem and apply an existing satisfiability solver or theorem prover to the problem,
- understand strengths and weaknesses of existing satisfiability solvers and theorem provers.
Learning outcomes
At the end of the course, students should:
- have working knowledge of propositional logic and first-order logic,
- be able to express real-world problems in a suitable logical formalism,
- be able to explain principles, algorithms, and underlying theoretical concepts of modern satisfiability solvers and theorem provers,
- be able to assess what kind of tool is relevant for their problem and apply an existing satisfiability solver or theorem prover to the problem,
- understand strengths and weaknesses of existing satisfiability solvers and theorem provers.
Syllabus
  • Propositional satisfiability: syntax and semantics of propositional logic , encoding of real-world problems, historical and modern satisfiability decision procedures, design and usage of modern satisfiability solvers, preprocessing techniques, proofs of unsatisfiability.
  • Satisfiability Modulo Theories: syntax and semantics of first-order logic without quantifiers; first-order theories relevant for description of systems, their decidability and complexity; CDCL(T) algorithm and theory solvers for selected first-order theories.
  • Reasoning with Quantifiers: syntax and semantics of first-order logic with quantifiers; encoding of real-world problems; first-order resolution, superposition, E-matching; implementation of proof search in modern theorem provers; quantifier elimination; quantifier instantiation.
  • Interactive Theorem Proving: formal foundations; practical usage of a state-of-the art theorem prover.
Literature
  • Handbook of satisfiability. Edited by Armin Biere. Amsterdam: IOS Press, 2009, xiii, 966. ISBN 9781586039295. info
Teaching methods
Lectures, homework.
Assessment methods
Homework, final written exam.
Language of instruction
English
Further Comments
Study Materials
The course is taught annually.
  • Enrolment Statistics (recent)
  • Permalink: https://is.muni.cz/course/fi/spring2024/IA085