Locality Transfer: From Constrained Axiomatizations to Reachability Predicates

ABSTRACT. In this paper, we build upon our previous work on using constrained clauses in order to finitely represent possibly infinite sets of clauses.

We explore theories and theory extensions that are axiomatized by sets of constrained clauses, and we characterize syntactic criteria for their locality. We have previously shown that constrained axiomatizations are local if they are saturated under a version of resolution. The appearing constraints often capture interesting properties like reachability or extensions thereof.

We extend this result by proving that locality of saturated axiomatizations is maintained if we enrich the base theory by introducing new predicates instead of using constraints for these properties. Often, these new predicates are reachability predicates.

Applications of these results include reasoning about data structures; we indicate how the ideas can be adapted for also handling certain theories with greatest/smallest fixpoints.