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.
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
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)