IA���: 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
▸ Friday, ��:��, D�
▸ language: English
▸ slides and a video recording will be available on 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
▸ resolution method for propositional logic
▸ resolution method for first-order logic
▸ Prolog
▸ proof calculi (natural deduction and tableaux) for first-order logic
▸ modal logic
▸ induction
▸ many-valued logic