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.
They are used everywhere in computer science:
▸ databases (SQL)
▸ regular expressions
▸ software 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
▸ Tuesday, 10:00, A318
▸ language: English
▸ slides and video recordings will be available in IS
Exercise classes
▸ exercises done by students
▸ come prepared
Examination
▸ final written exam (probably online)
▸ 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)