Decidability, Introduction Rules and Automata

TL;DR

This paper introduces a method to establish the decidability of provability in various inference systems by generalizing cut-elimination and automaton construction techniques.

Contribution

It provides a unified approach to prove decidability, combining existing methods into a generalized framework applicable to multiple inference systems.

Findings

Decidability of provability in several inference systems is established.

Automaton construction is used to recognize provable propositions.

The method generalizes existing techniques like cut-elimination.

Abstract

We present a method to prove the decidability of provability in several well-known inference systems. This method generalizes both cut-elimination and the construction of an automaton recognizing the provable propositions.