Publication

On Locality of One-Variable Axioms and Piecewise Combinations

2010
Reports

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.

Official source

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2010
Reports

Abstract

Official source

Related concepts (31)

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.

Tarski's axioms

Tarski's axioms, due to Alfred Tarski, are an axiom set for the substantial fragment of Euclidean geometry that is formulable in first-order logic with identity, and requiring no set theory (i.e., that part of Euclidean geometry that is formulable as an elementary theory). Other modern axiomizations of Euclidean geometry are Hilbert's axioms and Birkhoff's axioms. Early in his career Tarski taught geometry and researched set theory.

Related publications (1)

On Locality of One-Variable Axioms and Piecewise Combinations

Chat with Graph Search

Counterexample-Guided Focus