On Locality of One-Variable Axioms and Piecewise Combinations

Viktor Kuncak, Swen Jacobs
2010
Report or working paper

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.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (33)

Related publications (20)

Axiom

An axiom, postulate, or assumption is a statement that is taken to be true, to serve as a premise or starting point for further reasoning and arguments. The word comes from the Ancient Greek word ἀξίωμα (), meaning 'that which is thought worthy or fit' or 'that which commends itself as evident'. The precise definition varies across fields of study. In classic philosophy, an axiom is a statement that is so evident or well-established, that it is accepted without controversy or question.

Peano axioms

In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th-century Italian mathematician Giuseppe Peano. These axioms have been used nearly unchanged in a number of metamathematical investigations, including research into fundamental questions of whether number theory is consistent and complete.

Abelian extension

In abstract algebra, an abelian extension is a Galois extension whose Galois group is abelian. When the Galois group is also cyclic, the extension is also called a cyclic extension. Going in the other direction, a Galois extension is called solvable if its Galois group is solvable, i.e., if the group can be decomposed into a series of normal extensions of an abelian group. Every finite extension of a finite field is a cyclic extension.

Scaling Functional Synthesis and Repair

Emmanouil Koukoutos

Program synthesis was first proposed a few decades ago, but in the last decade it has gained increased momentum in the research community. The increasing complexity of software has dictated the urgent need for improved supporting tools that verify the soft ...

EPFL2019

Efficient Learning from Comparisons

Lucas Maystre

Humans are comparison machines: comparing and choosing an item among a set of alternatives (such as objects or concepts) is arguably one of the most natural ways for us to express our preferences and opinions. In many applications, the analysis of data con ...

EPFL2018

Embeddings of maximal tori in classical groups over fields of characteristic not 2 are the subject matter of several recent papers. The aim of the present paper is to give necessary and sufficient conditions for such an embedding to exist, when the base fi ...

Turpion Ltd2016