Decidability and Undecidability Results for Propositional Schemata
This addresses decidability issues in logic for researchers in automated reasoning, offering a compromise between expressivity and decidability, though it is incremental in extending known results.
The paper tackles the satisfiability problem for propositional formula schemata, showing it is undecidable in general but decidable for a class called bound-linear schemata, with a sound and complete proof procedure provided.
We define a logic of propositional formula schemata adding to the syntax of propositional logic indexed propositions and iterated connectives ranging over intervals parameterized by arithmetic variables. The satisfiability problem is shown to be undecidable for this new logic, but we introduce a very general class of schemata, called bound-linear, for which this problem becomes decidable. This result is obtained by reduction to a particular class of schemata called regular, for which we provide a sound and complete terminating proof procedure. This schemata calculus allows one to capture proof patterns corresponding to a large class of problems specified in propositional logic. We also show that the satisfiability problem becomes again undecidable for slight extensions of this class, thus demonstrating that bound-linear schemata represent a good compromise between expressivity and decidability.