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})$.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element