Decision procedures for extensions of the theory of arrays

The theory of arrays, introduced by McCarthy in his seminal paper “Towards a mathematical science of computation,” is central to Computer Science. Unfortunately, the theory alone is not sufficient for many important verification applications such as program analysis. Motivated by this observation, we study extensions of the theory of arrays whose satisfiability problem (i.e., checking the satisfiability of conjunctions of ground literals) is decidable. In particular, we consider extensions where the indexes of arrays have the algebraic structure of Presburger arithmetic and the theory of arrays is augmented with axioms characterizing additional symbols such as dimension, sortedness, or the domain of definition of arrays. We provide methods for integrating available decision procedures for the theory of arrays and Presburger arithmetic with automatic instantiation strategies which allow us to reduce the satisfiability problem for the extension of the theory of arrays to that of the theories decided by the available procedures. Our approach aims to re-use as much as possible existing techniques so as to ease the implementation of the proposed methods. To this end, we show how to use model-theoretic, rewriting-based theorem proving (i.e., superposition), and techniques developed in the Satisfiability Modulo Theories communities to implement the decision procedures for the various extensions.      

A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions

MLSS is a decidable sublanguage of set theory involving the predicates membership, set equality, set inclusion, and the operators union, intersection, set difference, and singleton.In this paper we extend MLSS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We prove that the resulting language is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of MLSS.     

Theory decision by decomposition

The topic of this article is decision procedures for satisfiability modulo theories (SMT) of arbitrary quantifier-free formulæ. We propose an approach that decomposes the formula in such a way that its definitional part, including the theory, can be compiled by a rewrite-based first-order theorem prover, and the residual problem can be decided by an SMT-solver, based on the Davis–Putnam–Logemann–Loveland procedure. The resulting decision by stages mechanism may unite the complementary strengths of first-order provers and SMT-solvers. We demonstrate its practicality by giving decision procedures for the theories of records, integer offsets and arrays, with or without extensionality, and for combinations including such theories.     

Unification in the Union of Disjoint Equational Theories: Combining Decision Procedures

Most of the work on the combination of unification algorithms for the union of disjoint equational theories has been restricted to algorithms that compute finite complete sets of unifiers.Thus the developed combination methods usually cannot be used to combine decision procedures,i.e., algorithms that just decide solvability of unification problems without computing unifiers.In this paper we describe a combination algorithm for decision procedures that works for arbitrary equational theories, provided that solvability of so–called unification problems with constant restrictions—a slight generalization of unification problems with constants—is decidable for these theories.As a consequence of this new method, we can, for example, show that generalA-unifiability, i.e.,solvability ofA-unification problems with free function symbols, is decidable. HereAstandsfor the equational theory of one associative function symbol.Our method can also be used to combine algorithms that compute finite complete sets of unifiers. Manfred Schmidt–Schauß' combination result, the until now most general result in this direction, can be obtained as a consequence of this fact.We also obtain the new result that unification in the union of disjoint equational theories is finitary, if general unification—i.e., unification of terms with additional free function symbols—is finitary in the single theories.     

Automatic decidability and combinability

Verification problems can often be encoded as first-order validity or satisfiability problems. The availability of efficient automated theorem provers is a crucial pre-requisite for automating various verification tasks as well as their cooperation with specialized decision procedures for selected theories, such as Presburger Arithmetic. In this paper, we investigate how automated provers based on a form of equational reasoning, called paramodulation, can be used in verification tools. More precisely, given a theory T axiomatizing some data structure, we devise a procedure to answer the following questions. Is the satisfiability problem of T decidable by paramodulation? Can a procedure based on paramodulation for T be efficiently combined with other specialized procedures by using the Nelson-Oppen schema? Finally, if paramodulation decides the satisfiability problem of two theories, does it decide satisfiability in their union?The procedure capable of answering all questions above is based on Schematic Saturation; an inference system capable of over-approximating the inferences of paramodulation when solving satisfiability problems in a given theory T. Clause schemas derived by Schematic Saturation describe all clauses derived by paramodulation so that the answers to the questions above are obtained by checking that only finitely many different clause schemas are derived or that certain clause schemas are not derived.     

Combining Non-Stably Infinite Theories

The Nelson-Oppen combination method combines decision procedures for first-order theories over disjoint signatures into a single decision procedure for the union theory. To be correct, the method requires that the component theories be stably infinite. This restriction makes the method inapplicable to many interesting theories such as, for instance, theories having only finite models.In this paper we provide a new combination method that can combine any theory that is not stably infinite with another theory, provided that the latter is what we call a shiny theory. Examples of shiny theories include the theory of equality, the theory of partial orders, and the theory of total orders.An interesting consequence of our results is that any decision procedure for the satisfiability of quantifier-free Σ-formulae in a Σ-theory T can always be extended to accept inputs over an arbitrary signature Ω Σ.     

Structured proof procedures

In this paper, we address the problem of enriching an interactive theorem prover with complex proof procedures. We show that the approach of building complex proof procedures out of deciders for (decidable) quantifier-free theories has many advantages: (i) deciders for quantifier-free theories provide powerful, high level functionalities which greatly simplify the activity of designing and implementing complex and higher level proof procedures; (ii) this approach is of wide applicability since most of the proof procedures are composed by steps of propositional reasoning intermixed with steps carrying out higher level strategical functionalities; (iii) decidability and efficiency are retained on important (decidable) subclasses, while they are often sacrificed by uniform proof strategies for the sake of generality; and finally (iv), from a software engineering perspective, the modularity of the procedures guarantees that any modification in the implementation can be accomplished locally. As a case study, we present and discuss a proof procedure for the existential fragment of first-order logic (prenex existential formulas without function symbols) built on top of a propositional decider.     

Recognizability,hypergraph operations,and logical types

We study several algebras of graphs and hypergraphs and the corresponding notions of equational sets and recognizable sets. We generalize and unify several existing results which compare the associated equational and recognizable sets. The basic algebra on relational structures is based on disjoint union and quantifier-free definable operations. We expand it to an equivalent one by adding operations definable with “few quantifiers”, i.e., operations that take into account local information about elements or tuples. We also consider monadic second-order transductions and we prove that the inverse image of a recognizable set under such a transduction is recognizable.     

Restricted compositions and permutations: From old to new Gray codes

Any Gray code for a set of combinatorial objects defines a total order relation on this set: x is less than y if and only if y occurs after x in the Gray code list. Let ? denote the order relation induced by the classical Gray code for the product set (the natural extension of the Binary Reflected Gray Code to k-ary tuples). The restriction of ? to the set of compositions and bounded compositions gives known Gray codes for those sets. Here we show that ? restricted to the set of bounded compositions of an interval yields still a Gray code. An n-composition of an interval is an n-tuple of integers whose sum lies between two integers; and the set of bounded n-compositions of an interval simultaneously generalizes product set and compositions of an integer, and so ? put under a single roof all these Gray codes.As a byproduct we obtain Gray codes for permutations with a number of inversions lying between two integers, and with even/odd number of inversions or cycles. Such particular classes of permutations are used to solve some computational difficult problems.     

Permutative rewriting and unification

Permutative rewriting provides a way of analyzing deduction modulo a theory defined by leaf-permutative equations. Our analysis naturally leads to the definition of the class of unify-stable axiom sets, in order to enforce a simple reduction strategy. We then give a uniform unification algorithm modulo theories E axiomatized this way. We prove that it computes complete sets of unifiers of simply exponential cardinality, and that the E-unification decision problem belongs to NP.     

NP-completeness of small conflict set generation for congruence closure

The efficiency of satisfiability modulo theories (SMT) solvers is dependent on the capability of theory reasoners to provide small conflict sets, i.e. small unsatisfiable subsets from unsatisfiable sets of literals. Decision procedures for uninterpreted symbols (i.e. congruence closure algorithms) date back from the very early days of SMT. Nevertheless, to the best of our knowledge, the complexity of generating smallest conflict sets for sets of literals with uninterpreted symbols and equalities had not yet been determined, although the corresponding decision problem was believed to be NP-complete. We provide here an NP-completeness proof, using a simple reduction from SAT.     

A Decision Procedure for a Sublanguage of Set Theory Involving Monotone, Additive, and Multiplicative Functions, I: The Two-Level Case

2LS is a decidable many-sorted set-theoretic language involving one sort for elements and one sort for sets of elements. In this paper we extend 2LS with constructs for expressing monotonicity, additivity, and multiplicativity properties of set-to-set functions. We call the resulting language 2LSmf. We prove that 2LSmf is decidable by reducing the problem of determining the satisfiability of its sentences to the problem of determining the satisfiability of sentences of 2LS. Furthermore, we prove that the language 2LSmf is stably infinite with respect to the sort of elements. Therefore, by using a many-sorted version of the Nelson–Oppen combination method, 2LSmf can be combined with other languages modeling the sort of elements.     

TSAT++: an Open Platform for Satisfiability Modulo Theories

This paper describes TSAT++, an open platform which realizes the lazy SAT-based approach to Satisfiability Modulo Theories (SMT). SMT is the problem of determining satisfiability of a propositional combination of T-literals, where T is a first-order theory for which a satisfiability procedure for a set of ground atoms is known. TSAT++ enjoys a modular design in which an enumerator and a theory-specific satisfiability checker cooperate in order to solve SMT. Modularity allows both different enumerators, and satisfiability checkers for different theories (or combinations of theories), to be plugged in, as far as they comply to a simple and well-defined interface. A number of optimization techniques are also implemented in TSAT++, which are independent of the modules used (and of the corresponding theory). Some experimental results are presented, showing that TSAT++, instantiated for Separation Logic, is competitive with, or faster than, state-of-the-art solvers for that very logic.     

E-unification with Constants vs. General E-unification

We present a solution to Problem #66 from the RTA open problem list. The question is whether there exists an equational theory E such that E-unification with constants is decidable but general E-unification is undecidable. The answer is positive and we show such a theory. The problem has several equivalent formulations, therefore the solution has many consequences. Our result also shows, that there exist two theories E ₁ and E ₂ over disjoint signatures, such that E ₁-unification with constants and E ₂-unification with constants are decidable, but (E ₁ ∪ E ₂)-unification with constants is undecidable.     

On decidability of monadic logic of order over the naturals extended by monadic predicates

A fundamental result of Büchi states that the set of monadic second-order formulas true in the structure (Nat,  <) is decidable. A natural question is: what monadic predicates (sets) can be added to (Nat,  <) while preserving decidability? Elgot and Rabin found many interesting predicates P for which the monadic theory of 〈Nat, <,  P〉 is decidable. The Elgot and Rabin automata theoretical method has been generalized and sharpened over the years and their results were extended to a variety of unary predicates. We give a sufficient and necessary model-theoretical condition for the decidability of the monadic theory of (Nat, <, P₁, … , P_n).We reformulate this condition in an algebraic framework and show that a sufficient condition proposed previously by O. Carton and W.Thomas is actually necessary. A crucial argument in the proof is that monadic second-order logic has the selection and the uniformization properties over the extensions of (Nat, <) by monadic predicates. We provide a self-contained proof of this result.     

Combining Sets with Cardinals

We introduce a quantifier-free set-theoretic language for combining sets with elements in the presence of the cardinality operator. We prove that the language is decidable by providing a combination method specifically tailored to the combination domain of sets, cardinal numbers, and elements. Our method uses as black boxes a decision procedure for the elements and a decision procedure for cardinal numbers. To be correct, our method requires that the theory of elements be stably infinite. However, we show that if we restrict set variables to range over finite sets only, then one can modify our method so that it works even when the theory of the elements is not stably infinite.     

Decidable metric logics

The common metric temporal logic for continuous time were shown to be insufficient, when it was proved that they cannot express a modality suggested by Pnueli. Moreover no finite temporal logic can express all the natural generalizations of this modality. It followed that if we look for an optimal decidable metric logic we must accept infinitely many modalities, or adopt a different formalism.Here we identify a fragment of the second order monadic logic of order with the “+1” function, that expresses all the Pnueli modalities and much more. Its main advantage over the temporal logics is that it enables us to say not just that within prescribed time there is a point where some punctual event will occur, but also that within prescribed time some process that starts now (or that started before, or that will start soon) will terminate. We prove that this logic is decidable with respect to satisfiability and validity, over continuous time. The proof depends heavily on the theory of compositionality. In particular every temporal logic that has truth tables in this logic is automatically decidable. We extend this result by proving that any temporal logic, that has all its modalities defined by means more general than truth tables, in a logic stronger than the one just described, has a decidable satisfiability problem. We suggest that this monadic logic can be the framework in which temporal logics can be safely defined, with the guarantee that their satisfiability problem is decidable.     

Abstractions for hybrid systems

We present a procedure for constructing sound finite-state discrete abstractions of hybrid systems. This procedure uses ideas from predicate abstraction to abstract the discrete dynamics and qualitative reasoning to abstract the continuous dynamics of the hybrid system. It relies on the ability to decide satisfiability of quantifier-free formulas in some theory rich enough to encode the hybrid system. We characterize the sets of predicates that can be used to create high quality abstractions and we present new approaches to discover such useful sets of predicates. Under certain assumptions, the abstraction procedure can be applied compositionally to abstract a hybrid system described as a composition of two hybrid automata. We show that the constructed abstractions are always sound, but are relatively complete only under certain assumptions.