Дисертації з теми "Satisfiability theory"

Many computational problems require reasoning about relational structures. Examples include high-level system design, architectural configuration of network systems, reasoning about ontologies, and verification of programs with linked data structures. Traditionally, relational models are translated to propositional formulas and then solved by leveraging SAT solvers. However, SAT solvers can only reason about problems within a finite scope, i.e, concrete cardinality bounds on the relations involved. SMT solvers, on the other hand, are efficient tools that can check automatically the satisfiability of complex constraints over several domains without scope restrictions. They are used as the back-end solvers in many verification tools. To break the limitation of bounded analysis, this thesis presents a many-sorted relational logic in SMT where relations of arity n are defined as sets of n-tuples with parametrized sorts for tuple elements. We define a version of this logic as a first-order theory of finite relations where relation terms are built from relation constants and variables, set operators, and relational operators such as join, transpose, product, and transitive closure. We also present a deductive calculus for that theory and provide proofs of refutation soundness and model soundness of our calculus. In addition, we implement the calculus as a relational solver in the SMT solver CVC4, expanding its already large set of built-in theories, and evaluate the relational solver in two applications: Alloy and Ontology, showing promising results. Moreover, with the goal of improving the performance of SMT solvers in general, we present a symmetry detection algorithm to detect symmetries in SMT formulas and present a symmetry breaking algorithm to generate blocking constraints that eliminate those symmetries. We then discuss an experimental evaluation of our implementation of these algorithms in CVC4 against SMT-LIB benchmarks.

La génération de stratégies pour les solveurs en Satisfiabilité Modulo des Théories (SMT) nécessite des outils théoriques et pratiques qui permettent aux utilisateurs d’exercer un contrôle stratégique sur les aspects heuristiques fondamentaux des solveurs de SMT, tout en garantissant leur performance. Nous nous intéressons dans cette thèse au solveur Z3 , l’un des plus efficaces lors des compétitions SMT (SMT-COMP). Dans les solveurs SMT, la définition d’une stratégie repose sur un ensemble de composants et paramètres pouvant être agencés et configurés afin de guider la recherche d’une preuve de (in)satisfiabilité d’une instance donnée. Dans cette thèse, nous abordons ce défi en définissant un cadre pour la génération autonome de stratégies pour Z3, c’est-à-dire un algorithme qui permet de construire automatiquement des stratégies sans faire appel à des connaissances d’expertes. Ce cadre général utilise une approche évolutionnaire (programmation génétique), incluant un système à base de règles. Ces règles formalisent la modification de stratégies par des principes de réécriture, les algorithmes évolutionnaires servant de moteur pour les appliquer. Cette couche intermédiaire permettra d’appliquer n’importe quel algorithme ou opérateur sans qu’il soit nécessaire de modifier sa structure, afin d’introduire de nouvelles informations sur les stratégies. Des expérimentations sont menées sur les jeux classiques de la compétition SMT-COMP
The Strategy Challenge in Satisfiability Modulo Theories (SMT) claims to build theoretical and practical tools allowing users to exert strategic control over core heuristic aspects of high-performance SMT solvers. In this work, we focus in Z3 Theorem Prover: one of the most efficient SMT solver according to the SMT Competition, SMT-COMP. In SMT solvers, the definition of a strategy relies on a set of tools that can be scheduled and configured in order to guide the search for a (un)satisfiability proof of a given instance. In this thesis, we address the Strategy Challenge in SMT defining a framework for the autonomous generation of strategies in Z3, i.e. a practical system to automatically generate SMT strategies without the use of expert knowledge. This framework is applied through an incremental evolutionary approach starting from basic algorithms to more complex genetic constructions. This framework formalise strategies modification as rewriting rules, where algorithms acts as enginess to apply them. This intermediate layer, will allow apply any algorithm or operator with no need to being structurally modified, in order to introduce new information in strategies. Validation is done through experiments on classic benchmarks of the SMT-COMP

Static program analysis is a core technology for both verifying and finding errors in programs but most static analyzers are complex pieces of software that are not without error. A Static analysis formalised as an abstract interpreter can be proved sound, however such proofs are significantly harder to do on the actual implementation of an analyser. To alleviate this problem we propose to generate Verification Conditions (VCs, formulae valid only if the results of the analyser are correct) and to discharge them using an Automated Theorem Prover (ATP). We generate formulae in Many-Sorted First-Order Logic (MSFOL), a logic that has been successfully used in deductive program verification. MSFOL is expressive enough to describe the results of complex analyses and to formalise the operational semantics of object-oriented languages. Using the same logic for both tasks allows us to prove the soundness of the VC generator using deductive verification tools. To ensure that VCs can be automatically discharged for complex analyses of the heap, we introduce a VC calculus that produces formulae belonging to a decidable fragment of MSFOL. Furthermore, to be able to certify different analyses with the same calculus, we describe a family of analyses with a parametric concretisation function and instrumentation of the semantics. To improve the reliability of ATPs, we also studied the result certification of Satisfiability Modulo Theory solvers, a family of ATPs dedicated to MSFOL. We propose a modular proof-system and a modular proof-verifier programmed and proved correct in Coq, that rely on exchangeable verifiers for each of the underlying theories.

The local search algorithm WSAT is one of the most successful algorithms for solving the archetypal NP-complete problem of satisfiability (SAT). It is notably effective at solving RANDOM-3-SAT instances near the so-called "satisfiability threshold", which are thought to be universally hard. However, WSAT still shows a peak in search cost near the threshold and large variations in cost over different instances. Why are solutions to the threshold instances so hard to find using WSAT? What features characterise threshold instances which make them difficult for WSAT to solve? We make a number of significant contributions to the analysis of WSAT on these high-cost random instances, using the recently-introduced concept of the backbone of a SAT instance. The backbone is the set of literals which are implicates of and instance. We find that the number of solutions predicts the cost well for small-backbone instances but is much less relevant for the large-backbone instances which appear near the threshold and dominate in the overconstrained region. We undertake a detailed study of the behaviour of the algorithm during search and uncover some interesting patterns. These patterns lead us to introduce a measure of the backbone fragility of an instance, which indicates how persistent the backbone is as clauses are removed. We propose that high-cost random instances for WSAT are those with large backbones which are also backbone-fragile. We suggest that the decay in cost for WSAT beyond the satisfiability threshold, which has perplexed a number of researchers, is due to the decreasing backbone fragility. Our hypothesis makes three correct predictions. First, that a measure of the backbone robustness of an instance (the opposite to backbone fragility) is negatively correlated with the WSAT cost when other factors are controlled for. Second, that backbone-minimal instances (which are 3-SAT instances altered so as to be more backbone-fragile) are unusually hard for WSAT. Third, that the clauses most often unsatisfied during search are those whose deletion has the most effect on the backbone.

Submitted by Marcos Roberto Gomes (mrobertosg@gmail.com) on 2017-06-22T15:28:21Z No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5)
Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-06-23T14:38:14Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5)
Approved for entry into archive by Divisão de Documentação/BC Biblioteca Central (ddbc@ufam.edu.br) on 2017-06-23T14:44:39Z (GMT) No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5)
Made available in DSpace on 2017-06-23T14:44:39Z (GMT). No. of bitstreams: 2 license_rdf: 0 bytes, checksum: d41d8cd98f00b204e9800998ecf8427e (MD5) Dissertacao_Rodrigo_Farias_Araujo.pdf: 2432590 bytes, checksum: a0accf6a453257550a0ea9f75b50b687 (MD5) Previous issue date: 2017-03-30
This work presents a new method of optimization applied to different classes of problems, such as non-convex and convex. The methodology consists in the use the counterexample generated from the model checking technique based on Boolean satisfiability theory (SAT) and satisfiability modulo theory (SMT), to guide the optimization process. Three algorithms of optimization are developed: Generic Algorithm, applied to any class of optimization problem, it will be used in the optimization of non-convex functions, Simplified Algorithm, used in the optimization of functions in which there is some previous knowledge, e. g., semi-defined or defined positive functions and Fast Algorithm, used to optimize convex functions. In addition, convergence proofs are provided for the respective algorithms. The algorithms are implemented using two model verifiers, CBMC which uses the SAT-based MiniSAT solver as back-end, and the ESBMC, which supports SMT-based solvers, such as Z3, Boolector and MathSAT. For perfomance evaluation, the algorithms are applied to a set of thirty functions taken from the literature and used to test optimization algorithms, they are also compared with traditional optimization algorithms usually used in solving non-convex optimization problems, such as genetic algorithm, particle swarm, pattern search, simulated annealing and nonlinear programming. Through the analysis of the results it can be concluded that the developed algorithms are suitable the classes of functions for which they were developed and have a higher rate of success in the search for the optimal value in comparison with the other algorithms. Finally, the developed methodology is applied to solve optimization problems in the context of the two-dimensional path planning for autonomous mobile robots.
Este trabalho apresenta um novo método de otimização aplicado a diferentes classes de problemas, como não-convexos e convexos. A metodologia consiste na utilização do contraexemplo gerado a partir da técnica de verificação de modelos, baseada na teoria de satisfatibilidade booleana (SAT) ou na teoria do módulo de satisfatibilidade (SMT), para guiar o processo de otimização. São desenvolvidos três algoritmos de otimização, são eles: Algoritmo Genérico, aplicado a qualquer classe de problema de otimização, neste será utilizado na otimização de funções não-convexas, Algoritmo Simplificado, empregado na otimização de funções nas quais tem-se algum conhecimento prévio, por exemplo, funções semi-definidas ou definidas positivas e Algoritmo Rápido, utilizado para otimização de funções convexas. Adicionalmente, são fornecidas as provas de convergência para os respectivos algoritmos. Os algoritmos são implementados utilizando dois verificadores de modelos, o CBMC que utiliza como back-end o solucionador MiniSAT baseado em SAT, e o ESBMC, que tem suporte aos solucionadores baseados em SMT, como: Z3, Boolector e MathSAT. Para avaliação de desempenho, os algoritmos são aplicados a um conjunto de trinta funções retiradas da literatura e utilizadas para teste de algoritmos de otimização, os mesmos também são comparados com algoritmos de otimização tradicionais usualmente empregados na resolução de problemas de otimização não-convexa, como: algoritmo genético, enxame de partícula, busca de padrões, recozimento simulado e programação não-linear. Através da análise dos resultados pode-se concluir que os algoritmos desenvolvidos são adequados as classes de funções para os quais foram desenvolvidos e possuem maior taxa de acerto na busca pelo valor ótimo em comparação com os outros algoritmos. Finalmente a metodologia desenvolvida é aplicada para resolver problemas de otimização no contexto de planejamento de caminhos bidimensionais para robô móveis autônomos.

Over the last two decades, chip design has been conducted at the register transfer (RT) Level using Hardware Descriptive Languages (HDL), such as VHDL and Verilog. The modeling at the behavioral level not only allows for better representation and understanding of the design, but also allows for encapsulation of the sub-modules as well, thus increasing productivity. Despite these benefits, validating a RTL design is not necessarily easier. Today, design validation is considered one of the most time and resource consuming aspects of hardware design. The high costs associated with late detection of bugs can be enormous. Together with stringent time to market factors, the need to guarantee the correct functionality of the design is more critical than ever. The work done in this thesis tackles the problem of RTL design validation and presents new frameworks for functional test generation. We use branch coverage as our metric to evaluate the quality of the generated test stimuli. The initial effort for test generation utilized simulation based techniques because of their scalability with design size and ease of use. However, simulation based methods work on input spaces rather than the DUT's state space and often fail to traverse very narrow search paths in large input spaces. To encounter this problem and enhance the ability of test generation framework, in the following work in this thesis, certain design semantics are statically extracted and recurrence relationships between different variables are mined. Information such as relations among variables and loops can be extremely valuable from test generation point of view. The simulation based method is hybridized with Z3 based symbolic backward execution engine with feedback among different stages. The hybridized method performs loop abstraction and is able to traverse narrow design paths without performing costly circuit analysis or explicit loop unrolling. Also structural and functional unreachable branches are identified during the process of test generation. Experimental results show that the proposed techniques are able to achieve high branch coverage on several ITC'99 benchmark circuits and their modified variants, with significant speed up and reduction in the sequence length.
Master of Science

This dissertation shows that satisfiability procedures are abstract interpreters. This insight provides a unified view of program analysis and satisfiability solving and enables technology transfer between the two fields. The framework underlying these developments provides systematic recipes that show how intuition from satisfiability solvers can be lifted to program analyzers, how approximation techniques from program analyzers can be integrated into satisfiability procedures and how program analyzers and satisfiability solvers can be combined. Based on this work, we have developed new tools for checking program correctness and for solving satisfiability of quantifier-free first-order formulas. These tools outperform existing approaches. We introduce abstract satisfaction, an algebraic framework for applying abstract interpre- tation to obtain sound, but potentially incomplete satisfiability procedures. The framework allows the operation of satisfiability procedures to be understood in terms of fixed point computations involving deduction and abduction transformers on lattices. It also enables satisfiability solving and program correctness to be viewed as the same algebraic problem. Using abstract satisfaction, we show that a number of satisfiability procedures can be understood as abstract interpreters, including Boolean constraint propagation, the dpll and cdcl algorithms, St ̊almarck’s procedure, the dpll(t) framework and solvers based on congruence closure and the Bellman-Ford algorithm. Our work leads to a novel understand- ing of satisfiability architectures as refinement procedures for abstract analyses and allows us to relate these procedures to independent developments in program analysis. We use this perspective to develop Abstract Conflict-Driven Clause Learning (acdcl), a rigorous, lattice-based generalization of cdcl, the central algorithm of modern satisfiability research. The acdcl framework provides a solution to the open problem of lifting cdcl to new prob- lem domains and can be instantiated over many lattices that occur in practice. We provide soundness and completeness arguments for acdcl that apply to all such instantiations. We evaluate the effectiveness of acdcl by investigating two practical instantiations: fp-acdcl, a satisfiability procedure for the first-order theory of floating point arithmetic, and cdfpl, an interval-based program analyzer that uses cdcl-style learning to improve the precision of a program analysis. fp-acdcl is faster than competing approaches in 80% of our benchmarks and it is faster by more than an order of magnitude in 60% of the benchmarks. Out of 33 safe programs, cdfpl proves 16 more programs correct than a mature interval analysis tool and can conclusively determine the presence of errors in 24 unsafe benchmarks. Compared to bounded model checking, cdfpl is on average at least 260 times faster on our benchmark set.

Ce mémoire est constitué de 3 parties.La NP-complétude de la satisfaction de combinaisons booléennes de contraintes de sous-arbres est démontrée dans l'article [Ven87] ; la partie I de ce mémoire étudie dans quelle mesure l'ajout de contraintes régulières laisse espérer conserver la complexité NP. Ce modèle étendu définit une nouvelle classe de langages dont l'expressivité est comparée à celle des Rigid Tree Automata [JKV11]. Puis un début de formalisation des t-dags est donné.Les patterns ont été étudiés, principalement du point de vue des contraintes sur les données qu'ils demandent. La partie II de ce mémoire les étudie plus finement, en mettant de côté les données. Les squelettes sont définis en tant qu'intermédiaire de calcul et le fait que leur syntaxe caractérise leur sémantique est démontré. Puis un lemme de pompage est donné dans un cas restreint, un autre dans le cas général est étudié et conjecturé. Ensuite des fragments de combinaisons booléennes de patterns sont comparés en expressivité pour terminer avec l'étude de la complexité des problèmes de model-checking, satisfaisabilité et DTD-satisfaisabilité sur les dits fragments.Le contenu de la partie III constitue l'article [FMS11], c'est la démonstration de la caractérisation des langages des automates fortement déterministes de niveau 2 par des systèmes d'équations récurrentes caténatives. Celle-ci utilise, entre autres, des techniques de réécriture, la notion d'inconnues non-réécrivables et les ordres noethériens. Cette caractérisation constitue le cas de base de la récurrence démontrée dans [Sén07]
This thesis is in 3 parts.The NP-completeness of satisfiability of boolean combinations of subtree constraints is shown in the article [Ven87] ; in the part I of this thesis, we study whether adding regular contraints lets hope for keeping the same complexity. This extended model defines a new class of languages which is compared in expressivity to the Rigid Tree Automata [JKV11]. Then a begining of formalisation of the t-dags is developped.The patterns have been studied mainly from the point of view of the constraints they demand on the data. The part II of this thesis study them more finely, by putting aside the data. The skeletons are defined as calculus intermediate and the characterisation holding between their syntax and their semantics is shown. Then a pumping lemma is prooved in a restreict case, another one is conjectured in the most general case. Then fragments of boolean combinations of patterns are compared in expressivity, this parts ends with the study of complexity of model-checking, satisfiability and DTD-satisfiability on these fragments.The content of part III constitutes the article [FMS11], it is the demonstration of the characterisation of strongly-deterministic 2-level pushdown automata by recurrent catenative equation systems. This proof uses in particular, some rewriting techniques, unrewritable unknowns and noetherian orders. This characterisation provides the base case of the recurrence shown in [Sén07]

Thesis (M. Sc.)--York University, 2005. Graduate Programme in Computer Science.
Typescript. Includes bibliographical references (leaves 90-94). Also available on the Internet. MODE OF ACCESS via web browser by entering the following URL: http://gateway.proquest.com/openurl?url_ver=Z39.88-2004 & res_dat=xri:pqdiss & rft_val_fmt=info:ofi/fmt:kev:mtx:dissertation & rft_dat=xri:pqdiss:MR11752.

M.Sc. (Mathematics)
This dissertation describes the solution toa specific logical problem, the satisfiability problem, in a logic of games called Alternating-time Temporal Logic (ATL). Computation Tree Logic (CTL) is a discrete branching-time temporal logic for reasoning about labelled transition systems. ATL extends CTL to describe gametheoretic situations, where multiple agents together determine the evolution of the system. In particular, ATL explicitly provides for describing the abilities of coalitions of agents in such systems. Weprovide an automata-based decision procedure for ATL by translating the satisfiability problem for an ATL formula to the nonemptiness problem for an Alternating Biichi 'free Automaton. The key result that enables this translation is a oundedbranching tree model theorem for ATL, proving that a satisfiable formula is also satisfiable in a tree model of bounded branching degree. In terms of complexity, we show that satisfiability in ATL is complete for exponential time, which agrees with the corresponding complexity result for the fragment CTL. Closely related to ATL is an independently developed family of modal logics, the Coalition Logics. The presented results also provide a satisfiability procedure for Extended Coalition Logic interpreted over strongly playable coalition models. The structure of the dissertation is as follows: • Chapter 1 is an introduction to the topic, provides an overview of the results and a preview of the dissertation. • Chapter 2 presents some mathematical preliminaries regarding trees, automata, fixed points and game theory. • Chapter 3 discusses CTL and in particular an automata-based satisfiability procedure for CTL. • Chapter 4 introduces Alternating-time Temporal Logic (ATL) as a logic of games. • Chapter 5 contains the main results of the dissertation: first we prove a boundedbranching tree model property for ATL. Then the construction of the required automaton for satisfiability checking is described. • Chapter 6 relates the present work to some other logics of games, and in particular the Coalition Logics. • Chapter 7 finalises the dissertation with a conclusion and a look at some future research directions that might be pursued following the present work.

This thesis describes a decision and minimization procedure for modal logic. The decision procedure answers the question of whether there exists a satisfying pointed model for a formula which obeys user-specified first-order conditions on the underlying frame. Then the minimization procedure produces a minimal model with respect to the number of worlds that satisfies the desired formula while obeying the requisite conditions on the underlying frame. A proof of correctness for the decision and minimization procedures is supplied, as well as a description of an implementation built upon the Enfragmo model expansion solver.
Graduate
0984
0318
wbkboyer@gmail.com

Expressiveness, and more recently, succinctness, are two central concerns of finite model theory and descriptive complexity theory. Succinctness is particularly interesting because it is closely related to the complexity-theoretic trade-off between parallel time and the amount of hardware. We develop new bounds on the expressiveness and succinctness of first-order logic with two variables on finite words, present a related result about the complexity of the satisfiability problem for this logic, and explore a new approach to the generalized star-height problem from the perspective of logical expressiveness. We give a complete characterization of the expressive power of first-order logic with two variables on finite words. Our main tool for this investigation is the classical Ehrenfeucht-Fra¨ıss´e game. Using our new characterization, we prove that the quantifier alternation hierarchy for this logic is strict, settling the main remaining open question about the expressiveness of this logic. A second important question about first-order logic with two variables on finite words is about the complexity of the satisfiability problem for this logic. Previously it was only known that this problem is NP-hard and in NEXP. We prove a polynomialsize small-model property for this logic, leading to an NP algorithm and thus proving that the satisfiability problem for this logic is NP-complete. Finally, we investigate one of the most baffling open problems in formal language theory: the generalized star-height problem. As of today, we do not even know whether there exists a regular language that has generalized star-height larger than 1. This problem can be phrased as an expressiveness question for first-order logic with a restricted transitive closure operator, and thus allows us to use established tools from finite model theory to attack the generalized star-height problem. Besides our contribution to formalize this problem in a purely logical form, we have developed several example languages as candidates for languages of generalized star-height at least 2. While some of them still stand as promising candidates, for others we present new results that prove that they only have generalized star-height 1.

Satisfiability (SAT) solvers are commonly used for a variety of applications, including hardware verification, software verification, theorem proving, debugging, and hard combinatorial problems. These applications rely on the efficiency and correctness of SAT solvers. When a problem is determined to be unsatisfiable, how can one be confident that a SAT solver has fully exhausted the search space? Traditionally, unsatisfiability results have been expressed using resolution or clausal proof systems. Resolution-based proofs contain perfect reconstruction information, but these proofs are extremely large and difficult to emit from a solver. Clausal proofs rely on rediscovery of inferences using a limited number of techniques, which typically takes several orders of magnitude longer than the solving time. Moreover, neither of these proof systems has been able to express contemporary solving techniques such as bounded variable addition. This combination of issues has left SAT solver authors unmotivated to produce proofs of unsatisfiability. The work from this dissertation focuses on validating satisfiability solver output in the unsatisfiability case. We developed a new clausal proof format called DRAT that facilitates compact proofs that are easier to emit and capable of expressing all contemporary solving and preprocessing techniques. Furthermore, we implemented a validation utility called DRAT-trim that is able to validate proofs in a time similar to that of the discovery time. The DRAT format has seen widespread adoption in the SAT community and the DRAT-trim utility was used to validate the results of the 2014 SAT Competition. DRAT-trim uses many advanced techniques to realize its performance gains, so why should the results of DRAT-trim be trusted? Mechanical verification enables users to model programs and algorithms and then prove their correctness with a proof assistant, such as ACL2. We designed a new modeling technique for ACL2 that combines efficient model execution with an agile and convenient theory. Finally, we used this new technique to construct a fast, mechanically-verified validation tool for proofs of unsatisfiability. This research allows SAT solver authors and users to have greater confidence in their results and applications by ensuring the validity of unsatisfiability results.
text

We show how the non-monotonic nature of common-sense reasoning can be formalised by circumscription. Various forms of circumscription are discussed. A new form of circumscription, namely naive circumscription, is introduced in order to facilitate the comparison of the various forms. Finally, some issues connected with the automation of circumscriptive reasoning are examined.
Computing
M. Sc. (Computer Science)

This thesis explores several methods which enable a first-order reasoner to conclude satisfiability of a formula modulo an arithmetic theory. The most general method requires restricting certain quantifiers to range over finite sets; such assumptions are common in the software verification setting. In addition, the use of first-order reasoning allows for an implicit representation of those finite sets, which can avoid scalability problems that affect other quantified reasoning methods. These new techniques form a useful complement to existing methods that are primarily aimed at proving validity. The Superposition calculus for hierarchic theory combinations provides a basis for reasoning modulo theories in a first-order setting. The recent account of ‘weak abstraction’ and related improvements make an mplementation of the calculus practical. Also, for several logical theories of interest Superposition is an effective decision procedure for the quantifier free fragment. The first contribution is an implementation of that calculus (Beagle), including an optimized implementation of Cooper’s algorithm for quantifier elimination in the theory of linear integer arithmetic. This includes a novel means of extracting values for quantified variables in satisfiable integer problems. Beagle won an efficiency award at CADE Automated theorem prover System Competition (CASC)-J7, and won the arithmetic non-theorem category at CASC-25. This implementation is the start point for solving the ‘disproving with theories’ problem. Some hypotheses can be disproved by showing that, together with axioms the hypothesis is unsatisfiable. Often this is relative to other axioms that enrich a base theory by defining new functions. In that case, the disproof is contingent on the satisfiability of the enrichment. Satisfiability in this context is undecidable. Instead, general characterizations of definition formulas, which do not alter the satisfiability status of the main axioms, are given. These general criteria apply to recursive definitions, definitions over lists, and to arrays. This allows proving some non-theorems which are otherwise intractable, and justifies similar disproofs of non-linear arithmetic formulas. When the hypothesis is contingently true, disproof requires proving existence of a model. If the Superposition calculus saturates a clause set, then a model exists, but only when the clause set satisfies a completeness criterion. This requires each instance of an uninterpreted, theory-sorted term to have a definition in terms of theory symbols. The second contribution is a procedure that creates such definitions, given that a subset of quantifiers range over finite sets. Definitions are produced in a counter-example driven way via a sequence of over and under approximations to the clause set. Two descriptions of the method are given: the first uses the component solver modularly, but has an inefficient counter-example heuristic. The second is more general, correcting many of the inefficiencies of the first, yet it requires tracking clauses through a proof. This latter method is shown to apply also to lists and to problems with unbounded quantifiers. Together, these tools give new ways for applying successful first-order reasoning methods to problems involving interpreted theories.