Menü
Positionsanzeige
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 2025W
Learning Outcomes
Competences
Students understand the fundamental concepts and methods of computational logic, i.e., those aspects of formal logic that can be supported by software and/or are relevant for software development. Students can model problems from various application domains by logical formulas and manually apply appropriate logical methods to solve simple instances of these problems. For the solution of more difficult instances, they are able to effectively utilize logical software tools.
Skills Knowledge
  • Propositional logic: computing truth tables and normal forms, simplifying by logical equivalences; deciding validity/satisfiability by various calculi/algorithms.
  • First-order logic: determining free variables, computing truth values of closed formulas over finite domains, simplifying by logical equivalences, computing normal forms; proving validity/satisfiability by various calculi/algorithms.
  • Equality: applying first-order logic inference rules for handling equality, transforming systems of equations into canonical term rewriting systems.
  • Decidable logical theories: deciding the satisfiability of formulas in various theories and in combinations of these theories.
  • Formalizing problems from various application domains by logical formulas, applying logical software tools for their solution: SAT solvers in propositional logic, automated theorem provers in first-order logic, SMT solvers in decidable logical theories.
Propositional logic: syntax and semantics, validity and satisfiability, logical equivalence, sequent calculus, resolution, DP algorithm, DPLL algorithm. First-order logic: syntax and semantics, validity and satisfiability, logical equivalence, sequent calculus, Gilmore algorithm, analytic tableaux, resolution. Equality: inference rules for equality reasoning, canonical term rewriting systems, Knuth-Bendix completion. Decidable logical theories: linear real arithmetic, Fourier-Motzkin elimination, the theory of equality with uninterpreted functions, the congruence closure method, the Nelson-Oppen method. Software for logical training (Sequent Calculus Trainer, Tree Proof Generator), SAT solving (MiniSat, Limboole), first-order theorem proving (Vampire), SMT solving (Z3).
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