Towards a Formal Verification of Courcelle's Theorem

The goal of this project is to complete a formal verification of Courcelle’s Theorem in Agda. On a high level, Courcelle’s theorem states that if you ask certain kinds of questions about certain kinds of graphs, you can get a certain kind of linear time answer. This theorem is important because it applies to many NP-hard problems, such as vertex cover and dominating set, and thus gives a quasi-linear algorithm for deciding certain questions (monadic second order logic questions) on a certain class of graphs (bounded treewidth graphs). Verification via proof assistants is a method of ensuring that either a mathematical proof or a program is correct, in a way that removes much of the possibility for human error. At this stage, we have completed our translation of the definitions given in Courcelle’s Theorem: A Game Theoretic Approach by Kneis et al. into Agda, which is the proof that we have chosen to verify. This involved reformulating several complex mathematical concepts into machine-checkable definitions. Specifically, we define symbols, signatures, structures, expansions of structures, restrictions of structures, tree decompositions, MSO formulas, isomorphisms of structures, model checking games, extended model checking games, equivalence between game positions and subgames, and finally a notion of a reduced game. The bulk of this thesis document is a detailed explanation of the fact that the mathematical definitions we formalize correspond to the way we encode them. This is in an effort to convince the reader that, once we do finish the complete proof, it will be correct since our definitions are correct, for the only way a proof assistant can be incorrect is by