Nelson Oppen combination as a rewrite theory

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.

Name thesis:degree_name

M.S.

Level thesis:degree_level

Thesis

Discipline thesis:degree_discipline

Mathematics

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2018

Author dc:creator

• Rodrigues, Nishant

Contributors dc:contributor

• Meseguer, José

• Satisfiability Module Theories
• SMT
• Automated Theorem Proving
• Nelson-Oppen

Statement dc:rights

• Copyright 2018 Nishant Rodrigues

Language dc:language

en

Handle dc:identifier

http://hdl.handle.net/2142/101601

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/101601