000148180 001__ 148180
000148180 005__ 20180913055736.0
000148180 037__ $$aREP_WORK
000148180 245__ $$aOn Locality of One-Variable Axioms and Piecewise Combinations
000148180 269__ $$a2010
000148180 260__ $$c2010
000148180 300__ $$a26
000148180 336__ $$aReports
000148180 520__ $$aLocal 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. 
000148180 6531_ $$adecision procedures
000148180 6531_ $$alocal theory extensions
000148180 6531_ $$aSMT
000148180 6531_ $$acombination
000148180 6531_ $$averification
000148180 700__ $$aJacobs, Swen
000148180 700__ $$0240031$$aKuncak, Viktor$$g177241
000148180 8564_ $$s270138$$uhttps://infoscience.epfl.ch/record/148180/files/JacobsKuncak-OneVariable.pdf$$yn/a$$zn/a
000148180 909C0 $$0252019$$pLARA$$xU11739
000148180 909CO $$ooai:infoscience.tind.io:148180$$pIC$$preport
000148180 937__ $$aEPFL-REPORT-148180
000148180 973__ $$aEPFL$$sPUBLISHED
000148180 980__ $$aREPORT