<p> A core technique of modern tools for formally reasoning about computing systems is generating and dispatching queries to automated theorem provers, including Satisfiability Modulo Theories (SMT) provers. SMT provers aim at the tight integration of decision procedures for propositional satisfiability and decision procedures for fixed first-order theories &ndash; known as theory solvers. This thesis presents several advancements in the design and implementation of theory solvers for quantifier-free linear real, integer, and mixed integer and real arithmetic. These are implemented within the SMT system CVC4. We begin by formally describing the Satisfiability Modulo Theories problem and the role of theory solvers within CVC4. We discuss known techniques for building solvers for quantifier-free linear real, integer, and mixed integer and real arithmetic around the Simplex for SMT algorithm. We give several small improvements to theory solvers using this algorithm and describe the implementation and theory of this algorithm in detail. To extend the class of problems that the theory solver can robustly support, we borrow and adapt several techniques from linear programming (LP) and mixed integer programming (MIP) solvers which come from the tradition of optimization. We propose a new decision procedure for quantifier-free linear real arithmetic that replaces the Simplex for SMT algorithm with a variant of the Simplex algorithm that performs a form of optimization &ndash; minimizing the sum of infeasibilties. In this thesis, we additionally describe techniques for leveraging LP and MIP solvers to improve the performance of SMT solvers without compromising correctness. Previous efforts to leverage such solvers in the context of SMT have concluded that in addition to being potentially unsound, such solvers are too heavyweight to compete in the context of SMT. We present an empirical comparison against other state-of-the-art SMT tools to demonstrate the effectiveness of the proposed solutions.</p>

<p>Abstract models of computation, such as Turing machines, &lambda;-calculus and logic gates, allow us to express computation without being concerned about the underlying technology that realizes them in the physical world. These models embrace a classical worldview wherein computation is essentially irreversible. From the perspective of quantum physics however, the physical world is one where every fundamental interaction is essentially reversible and various quantities such as energy, mass, angular momentum are conserved. Thus the irreversible abstractions we choose as the basis of our most primitive models of computing are at odds with the underlying reversible physical reality and hence our thesis: By embracing irreversible physical primitives, models of computation have also implicitly included a class of computational effects which we call information effects. </p><p> To make this precise, we develop an information preserving model of computation (in the sense of Shannon entropy) wherein the process of computing does not gain or lose information. We then express information effects in this model using an arrow meta-language, in much the same way that we model computational effects in the &lambda;-calculus using a monadic metalanguage. A consequence of this careful treatment of information, is that we effectively capture the gap between reversible computation and irreversible computation using a type-and-effect system. </p><p> The treatment of information effects has a parallel with open and closed systems in physics. Closed physical systems conserve mass and energy and are the basic unit of study in physics. Open systems interact with their environment, possibly exchanging matter or energy. These interactions may be thought of as effects that modify the conservation properties of the system. Computations with information effects are much like open systems and they can be converted into pure computations by making explicit the surrounding information environment that they interact with. </p><p> Finally, we show how conventional irreversible computation such as the &lambda;-calculus can be embedded into this model, such that the embedding makes the implicit information effects of the &lambda;-calculus explicit. </p>

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é 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.

Thesis (Ph. D.)--Georgia State University, 2005. / 1 electronic text (119 p. : ill.) : digital, PDF file. Title from title screen. Rajshekhar Sunderraman, committee chair; Yan-Qing Zhang, Anu Bourgeois, Lifeng Ding, committee members. Description based on contents viewed Apr. 3, 2007. Includes bibliographical references (p. 112-119).

Constraint problems are a powerful framework in which many common combinatorial problems can be expressed. Examples include graph colouring problems, Boolean satisfaction, graph cut problems, systems of equations, and many more. One typically distinguishes between constraint satisfaction problems (CSPs), which model strictly decision problems, and so-called valued constraint satisfaction problems (VCSPs), which also include optimisation problems. A key open problem in this field is the long-standing dichotomy conjecture by Feder and Vardi. It claims that CSPs only fall into two categories: Those that are NP-complete, and those that are solvable in polynomial time. This stands in contrast to Ladner's theorem, which, assuming P$\neq$NP, guarantees the existence of problems that are neither NP-complete, nor in P, making CSPs an exceptional class of problems. While the Feder-Vardi conjecture is proven to be true in a number of special cases, it is still open in the general setting. (Recent claims affirming the conjecture are not considered here, as they have not been peer-reviewed yet.) In this thesis, we approach the complexity of constraint problems from a descriptive complexity perspective. Namely, instead of studying the computational resources necessary to solve certain constraint problems, we consider the expressive power necessary to define these problems in a logic. We obtain several results in this direction. For instance, we show that Schaefer's dichotomy result for the case of CSPs over the Boolean domain can be framed as a definability result: Either a CSP is definable in fixed-point logic with rank (FPR), or it is NP-hard. Furthermore, we show that a dichotomy exists also in the general case. For VCSPs over arbitrary domains, we show that a VCSP is either definable in fixed-point logic with counting (FPC), or it is not definable in infinitary logic with counting. We show that these definability dichotomies also have algorithmic implications. In particular, using our results on the definability of VCSPs, we prove a dichotomy on the number of levels in the Lasserre hierarchy necessary to obtain an exact solution: For a finite-valued VCSP, either it is solved by the first level of the hierarchy, or one needs $\Omega(n)$ levels. Finally, we explore how other methods from finite model theory can be useful in the context of constraint problems. We consider pebble games for finite variable logics in this context, and expose new connections between CSPs, pebble games, and homomorphism preservation results.

This paper investigates the relationship between the theory of belief revision and Lindenbaum-Tarski algebras for propositional logic. The intent is to represent the revision function described by the AGM-postulates algebraically. The AGM theory is based on deductively closed sets, which are characterizable as generated filters in the algebra as well as depictable in the corresponding Hasse diagram. This fact is shown by proving that a partial order is definable for the algebra, that this order is the consequence relation of propositional calculus and that the generated filters are deductively closed. Furthermore, an alternative, but equivalent approach to the AGM theory is introduced, the revision proposed by Katsuno and Mendelzon, which characterizes the deductively closed sets as propositional formulae. This correspondence follows naturally from the behaviour of filters and can be applied without problems to define the functions of the AGM framework in the Lindenbaum-Tarski algebra. The visualization of partially ordered sets as a Hasse diiagram is used to depict an example of a belief revision. Lastly, some combinatorical calculations are introduced to determine the number of possible solution candidates for a belief revision.