Rewrite Closure and CF Hedge Automata - Jacquemard, Florent; Rusinowitch, Michaël
We introduce an extension of hedge automata called bidimensional context-free hedge automata, proposing a new uniform representation of vertical and horizontal computation steps in unranked ordered trees. The class recognized languages is shown to be preserved by rewrite closure with inverse-monadic rules. We also extend the parameterized rewriting rules used for modeling the W3C XQuery Update Facility in previous works, by the possibility to insert a new parent node above a given node. We show that the rewrite closure of hedge automata languages with these extended rewriting systems are context-free hedge languages.
Automatic Decidability for Theories Modulo Integer Offsets - Tushkanova, Elena; Ringeissen, Christophe; Giorgetti, Alain; Kouchnarenko, Olga
Many verification problems can be reduced to a satisfiability problem modulo theories. For building satisfiability procedures the rewriting-based approach uses a general calculus for equational reasoning named superposition. Schematic superposition, in turn, provides a mean to reason on the derivations computed by superposition. Until now, schematic superposition was only studied for standard superposition. We present a schematic superposition calculus modulo a fragment of arithmetics, namely the theory of Integer Offsets. This new schematic calculus is used to prove the decidability of the satisfiability problem for some theories extending Integer Offsets. We illustrate our theoretical contribution on theories representing extensions of...