Search

• < Previous
• 1
• Next >

---

The logical strength of B\"uchi's decidability theorem

Leszek Kołodziejczyk ; Henryk Michalewski ; Pierre Pradic ; Michał Skrzypczak.

We study the strength of axioms needed to prove various results related to automata on infinite words and B\"uchi's theorem on the decidability of the MSO theory of $(N, {\le})$. We prove that the following are equivalent over the weak second-order arithmetic theory $RCA_0$: (1) the induction&nbsp;[&hellip;]

---

A Curry-Howard Approach to Church's Synthesis

Pierre Pradic ; Colin Riba.

Church's synthesis problem asks whether there exists a finite-state stream transducer satisfying a given input-output specification. For specifications written in Monadic Second-Order Logic (MSO) over infinite words, Church's synthesis can theoretically be solved algorithmically using automata and&nbsp;[&hellip;]

---