We describe the system RegStab (for regular schemata tableau) that solves the satisfiability problem for a class of propositional schemata. Our formalism extends propositional logic by considering indexed propositions (such as $P_1,P_{{i}},P_{{j}+1},\ldots$) and iterated connectives (e.g. $\bigvee_{i={i}}^{n} \phi$). The indices and bounds are linear arithmetic expressions (possibly containing variables, interpreted as integers). Our system allows one to check the satisfiability of sequences of formulae such as $(\bigvee_{{i}=1}^{n} P_{i}) \wedge (\bigwedge_{{i}=1}^{n} \neg P_{i})$.

References in zbMATH (referenced in 1 article , 1 standard article )

Showing result 1 of 1.
Sorted by year (citations)

  1. Aravantinos, Vincent; Caferra, Ricardo; Peltier, Nicolas: RegSTAB: a SAT solver for propositional schemata (2010)