Moritz Lichter
Master Thesis: Decidability of S1S in Constructive Type Theory
Author: Moritz Lichter
Advisor: Prof. Dr. Gert Smolka
Abstract
We study monadic second order logic of (ℕ, <), short S1S, in the constructive type theory of Coq. We focus on decidability of satisfiability and on logical decidability of satisfaction. We show both properties by translating S1S formulas to Büchi automata. This translation requires complementation of Büchi automata. While the complementation operation can be defined, proving it correct is not possible constructively.
We localize the property not provable in general and separate it in admissible sequence structures. AS structures come with their own representation of infinite words and a proof for the separated property.
We verify the translation of formulas to Büchi automata and show decidability of satisfiability and logical decidability of satisfaction for all AS structures.
We consider two AS structures: Ultimately periodic words are admissible constructively. All infinite words are only admissible assuming Additive Ramsey. Additive Ramsey is a weakening of Ramsey's Theorem. Given Additive Ramsey, an S1S formula is ultimately periodically satisfiable if and only if it is satisfiable in general.
Additive Ramsey is a necessary assumption because Additive Ramsey, closure under complement of Büchi automata, and logical decidability of satisfaction in S1S are equivalent. Moreover, the three properties are independent in constructive type theory. All results are formalized and verified in a Coq development of about 7000 lines.
Materials
Legal notice, Privacy policy
