IA008: Computational Logic
Introduction
Achim Blumensath
blumens@fi.muni.cz
Faculty of Informatics, Masaryk University, Brno
Why Logic?
Logics are formal languages to make statements about
mathematical objects.
Why Logic?
Logics are formal languages to make statements about
mathematical objects.
吀hey are used everywhere in computer science:
▸ databases (SQL)
▸ regular expressions
▸ so昀tware verification, hardware verification
▸ controller synthesis
▸ type systems
▸ SAT-solvers (optimisation)
▸ theorem provers
Basic logic problems
Basic logic problems
Model Checking
Given a model M and a formula φ, check whether M ⊧ φ.
Basic logic problems
Model Checking
Given a model M and a formula φ, check whether M ⊧ φ.
Satisfiability
Given a formula φ, check whether there is some model M with
M ⊧ φ.
Course organisation
Lectures
▸ 吀hursday, 10:00, D1
▸ language: English
▸ slides and video recordings will be available in IS
Exercise classes
▸ exercises done by students
▸ come prepared
Examination
▸ final written exam
▸ in English
▸ k and z completion possible
Prerequisites
▸ basic knowledge of logic
▸ propositional and first-order logic
▸ formula, model, satisfaction relation, entailment relation
▸ syntactic normal forms
Topics covered
▸ propositional logic, resolution
▸ first-order logic, proof calculi (tableaux and natural deduction)
▸ Prolog, databases
▸ expressive power, back-and-forth arguments
▸ modal logic
▸ induction
▸ many-valued logic (if time permits)