| Detailed information |
| Original study plan |
Bachelor's programme Technical Mathematics 2023W |
| Objectives |
Students receive an introduction to computational logic, i.e., to those aspects of logic that can be supported by software and/or are relevant for software development: satisfiability solving in propositional logic, computer-supported and fully automated proving in first-order logic, and decision procedures for certain (combinations of) logical theories. In line with the topic of this course, the theory will be explained with the help of software that implements this theory. Furthermore, we will present computational tools that are actually used in real life and demonstrate their practical application.
|
| Subject |
- Propositional Logic: Syntax and Semantics, Proofs, Modern SAT Solving,
Applications of SAT Solving.
- First-Order Logic: Syntax and Semantics, Proofs, the Method of Analytic Tableaux, the Resolution Method, Reasoning about Equality, Software for Proving.
- SMT Solving: Decidable Theories, Combining Decision Procedures.
|
| Criteria for evaluation |
Written exam at the end of the semester.
|
| Methods |
Presentations with slides and software demonstrations; we offer accompanying exercises where problems are partially solved with the help of software.
|
| Language |
English |
| Study material |
- Lecture slides.
- John Harrison: Handbook of Practical Logic and Automated Reasoning.
- Jean H. Gallier: Logic for Computer Science - Foundations of Automated
Theorem Proving.
- Melvin Fitting: First-Order Logic and Automated Theorem Proving.
- Aaron R. Bradley, Zahor Manna: The Calculus of Computation - Decision
Procedures with Applications to Verification.
- Daniel Kroening, Ofer Strichman: Decision Procedures - An Algorithmic
Point of View.
|
| Changing subject? |
No |
| Further information |
https://risc.jku.at/courses/
|
| Corresponding lecture |
(*)TM1PEKVSWEN: KV Software Engineering (3 ECTS)
|
