report
On Locality of One-Variable Axioms and Piecewise Combinations
2010
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.
Type
report
Author(s)
Jacobs, Swen
Date Issued
2010
Total of pages
26
Written at
EPFL
EPFL units
Available on Infoscience
April 7, 2010
Use this identifier to reference this record