On Locality of One-Variable Axioms and Piecewise Combinations

paper ps   
Local theory extensions provide a complete and efficient way for reasoning about satisfiability of certain kinds of universally quantified formulas modulo a background theory. They are therefore useful in automated reasoning, software verification, and synthesis. In this paper, we 1) provide a sufficient condition for locality of axioms with one variable specifying functions and relations, 2) show how to obtain local axiomatizations from non-local ones in some cases, 3) show how to obtain piecewise combination of different local theory extensions.

Citation

Swen Jacobs and Viktor Kuncak. On locality of one-variable axioms and piecewise combinations. Technical Report EPFL-REPORT-148180, EPFL, April 2010.

BibTex Entry

@techreport{JacobsKuncak10LocalityofOneVariableAxioms,
  author = {Swen Jacobs and Kuncak, Viktor},
  title = {On Locality of One-Variable Axioms and Piecewise Combinations},
  institution = {EPFL},
  year = 2010,
  number = {EPFL-REPORT-148180},
  month = {April},
  abstract = {Local theory extensions provide a complete and efficient way for reasoning about satisfiability of certain kinds of universally quantified formulas modulo a background theory. They are therefore useful in automated reasoning, software verification, and synthesis. In this paper, we 1) provide a sufficient condition for locality of axioms with one variable specifying functions and relations, 2) show how to obtain local axiomatizations from non-local ones in some cases, 3) show how to obtain piecewise combination of different local theory extensions.}
}