A Tableaux-Based Decision Procedure for Multi-parameter Propositional Schemata

The class of

regular propositional schemata

, discovered by Aravantinos et al. [4], is a major advancement towards more expressive classes of inductive theorems with a decidable satisfiability problem. Though more expressive than previously known decidable classes outlined by Kapur & Giesl[17], it still requires the burdensome restriction of induction with only one free parameter. In general, unrestricted usage of multiple free parameters in schematic formulae is undecidable for satisfiability [2]. In later work, Aravantinos et al. [6] introduced

normalized clause sets

which have a decision procedure for satisfiability and allow for restricted usage of multiple parameters. In our work, we investigate classes of propositional schemata which allow for multiple free parameters and are more expressive than regular schemata. Specifically, the classes we investigate have a decision procedure for satisfiability testing without requiring the additional theoretical machinery of normalized clause sets. Thus, allowing one to avoid conversion to CNF formulae. Both of the classes we introduce,

linked schemata

and

pure overlap schemata

use the machinery introduced in the earlier works of Aravantinos et al.[4] with only a slight change to the decision procedure.