Add to ORKGAbstract. Local theory extensions provide a complete and efficient way for reasoning about satisfiability of certain kinds of universally quanti-fied formulas modulo a background theory. They are therefore useful in automated reasoning, software verification, and synthesis. In this pa-per, 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.
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and mo...
In this paper we study interpolation in local extensions of a base theory. We identify situations in...
In this paper we show that subsumption problems in many lightweight description logics (including ${...
Local theory extensions provide a complete and efficient way for reasoning about satisfiability of c...
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and mo...
Many problems in mathematics and computer science can be reduced to proving the satisfiability of co...
We present a general framework which allows to identify complex theories important in verification f...
Verification problems are often expressed in a language which mixes several theories. A natural ques...
Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions...
The goal of this paper is to illustrate the wide applicability in verification of results on local r...
Abstract. To support verification of expressive properties of functional programs, we consider algeb...
Many problems in computer science can be reduced to proving the satisfiability of conjunctions of li...
Abstract. Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories ...
Abstract. Well-known theorems of Hanf's and Gaifman's establishing locality of rst-order d...
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and mo...
In this paper we study interpolation in local extensions of a base theory. We identify situations in...
In this paper we show that subsumption problems in many lightweight description logics (including ${...
Local theory extensions provide a complete and efficient way for reasoning about satisfiability of c...
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and mo...
Many problems in mathematics and computer science can be reduced to proving the satisfiability of co...
We present a general framework which allows to identify complex theories important in verification f...
Verification problems are often expressed in a language which mixes several theories. A natural ques...
Many problems occurring in verification can be reduced to proving the satisfiability of conjunctions...
The goal of this paper is to illustrate the wide applicability in verification of results on local r...
Abstract. To support verification of expressive properties of functional programs, we consider algeb...
Many problems in computer science can be reduced to proving the satisfiability of conjunctions of li...
Abstract. Satisfiability Modulo Theories (SMT) solvers incorporate decision procedures for theories ...
Abstract. Well-known theorems of Hanf's and Gaifman's establishing locality of rst-order d...
In this paper we study theory combinations over non-disjoint signatures in which hierarchical and mo...
In this paper we study interpolation in local extensions of a base theory. We identify situations in...
In this paper we show that subsumption problems in many lightweight description logics (including ${...