16948

Video URL

https://simons.berkeley.edu/talks/logic

A Tutorial on Logic, With an Emphasis on the Connections With Automata Theory

(2021). A Tutorial on Logic, With an Emphasis on the Connections With Automata Theory. The Simons Institute for the Theory of Computing. https://simons.berkeley.edu/talks/logic

A Tutorial on Logic, With an Emphasis on the Connections With Automata Theory. The Simons Institute for the Theory of Computing, Jan. 25, 2021, https://simons.berkeley.edu/talks/logic 

          @misc{ scivideos_16948,
            doi = {},
            url = {https://simons.berkeley.edu/talks/logic},
            author = {},
            keywords = {},
            language = {en},
            title = {A Tutorial on Logic, With an Emphasis on the Connections With Automata Theory},
            publisher = {The Simons Institute for the Theory of Computing},
            year = {2021},
            month = {jan},
            note = {16948 see, \url{https://scivideos.org/Simons-Institute/16948}}
          }
Mikolaj Bojańczyk (University of Warsaw)
Talk number16948
Source RepositorySimons Institute
Subject

Abstract

This is a 3 part tutorial about logic. It is organised around algorithms for checking if a formula is true in a model.There are two central variants of this problem. In the model checking problem    we are given the model and the formula, and we want to know it the formula is true in the model. In the satisfiability (dually, validity) problem    we are only given the formula, and we want to know if it is true in some (dually, every) model (perhaps from some fixed class of models). There are three parts of the tutorial (each set of slides contains a soundtrack): Part 1 (slides ) discusses the variant of the model checking problem where the model is fixed and only the formula is given on the input. (This is also known as deciding the theory of the model.)  I will particularly focus on cases where the problem can be solved using automata, and hence the corresponding logic is going to be monadic second-order logic, which is an old friend of automata. Part 2 (slides) discusses the satisfiability problem. Here, again, the main focus is on variants of the problem that can be solved using automata, namely monadic second-order logic on words, trees and graphs of bounded treewidth. Part 2 (slides), soundtrack coming Jan 20 morning) discusses the variant of the model checking problem where the formula is fixed and the model is the input. Apart from results that use automata (mainly Courcelle’s theorem about MSO model checking on graphs of bounded treewidth), I will also discuss some results about first-order logic on sparse graph classes.