Inhalt

[ 201COMACOLV18 ] VL Computational Logic

Versionsauswahl
(*) Unfortunately this information is not available in english.
Workload Education level Study areas Responsible person Hours per week Coordinating university
3 ECTS B2 - Bachelor's programme 2. year Mathematics Wolfgang Schreiner 2 hpw Johannes Kepler University Linz
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)
On-site course
Maximum number of participants -
Assignment procedure Direct assignment