Files in this item



application/pdfRODRIGUES-THESIS-2018.pdf (161kB)
(no description provided)PDF


Title:Nelson Oppen combination as a rewrite theory
Author(s):Rodrigues, Nishant
Advisor(s):Meseguer, José
Department / Program:Mathematics
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Satisfiability Module Theories
Automated Theorem Proving
Abstract:Solving Satisfiability Modulo Theories (SMT) problems in a key piece in automating tedious mathematical proofs. It involves deciding satisfiability of formulas of a decidable theory, which can often be reduced to solving systems of equalities and disequalities, in a variety of theories such as linear and non-linear real and integer arithmetic, arrays, uninterpreted and Boolean algebra. While solvers exist for many such theories or their subsets, it is common for interesting SMT problems to span multiple theories. SMT solvers typically use refinements of the Nelson-Oppen combination method, an algorithm for producing a solver for the quantifier free fragment of the combination of a number of such theories via cooperation between solvers of those theories, for this case. Here, we present the Nelson-Oppen algorithm adapted for an order-sorted setting as a rewriting logic theory. We implement this algorithm in the Maude System and instantiate it with the theories of real and integer matrices to demonstrate its use in automated theorem proving, and with hereditarily finite sets with reals to show its use with non-convex theories. This is done using both SMT solvers written in Maude itself via reflection (Variant-based satisfiability) and using external solvers (CVC4 and Yices). This work can be considered a first step towards building a rich ecosystem of cooperating SMT solvers in Maude, that modeling and automated theorem proving tools typically written using the Maude System can leverage.
Issue Date:2018-07-19
Rights Information:Copyright 2018 Nishant Rodrigues
Date Available in IDEALS:2018-09-27
Date Deposited:2018-08

This item appears in the following Collection(s)

Item Statistics