Search

• < Previous
• 1
• Next >

---

Small Stone in Pool

Samuel R. Buss ; Leszek Aleksander Kolodziejczyk.

The Stone tautologies are known to have polynomial size resolution refutations and require exponential size regular refutations. We prove that the Stone tautologies also have polynomial size proofs in both pool resolution and the proof system of regular tree-like resolution with input lemmas&nbsp;[&hellip;]

---

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;]

---