{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/101601"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/101601","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Nelson Oppen combination as a rewrite theory","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.","abstract_html":"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.","abstract_has_math":false,"creators":["Rodrigues, Nishant"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"M.S.","degree_level":"Thesis","degree_discipline":"Mathematics","degree_department":null,"school":null,"contributors":["Meseguer, José"],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2018,"date_issued":"2018-09-27T16:17:55Z","date_published":"2018-09-27T16:17:55Z","updated_at":"2026-07-22T22:24:40Z","subjects":["Satisfiability Module Theories","SMT","Automated Theorem Proving","Nelson-Oppen"],"languages":["en"],"rights":["Copyright 2018 Nishant Rodrigues"],"rights_urls":[],"identifier_entries":[]},"links":{"outbound_url":"http://hdl.handle.net/2142/101601","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Meseguer, José"]},{"key":"dc:creator","label":"Author","values":["Rodrigues, Nishant"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2018-09-27T16:17:55Z","2018-07-19","2018-08"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Mathematics"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["M.S."]},{"key":"thesis:institution_name","label":"Thesis Institution Name","values":["University of Illinois at Urbana-Champaign"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Satisfiability Module Theories","SMT","Automated Theorem Proving","Nelson-Oppen"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["en"]},{"key":"dc:rights","label":"Dc Rights","values":["Copyright 2018 Nishant Rodrigues"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/101601"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-09-27 without embargo terms","The student, Nishant Rodrigues, accepted the attached license on 2018-07-17 at 05:43.","The student, Nishant Rodrigues, submitted this Thesis for approval on 2018-07-17 at 05:53.","This Thesis was approved for publication on 2018-07-19 at 08:53.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12898 on 2018-09-27 at 10:48:54","Made available in DSpace on 2018-09-27T16:17:55Z (GMT). No. of bitstreams: 2 RODRIGUES-THESIS-2018.pdf: 160742 bytes, checksum: 883d95baf0a9eef1be969d2c42b7eef8 (MD5) LICENSE.txt: 4214 bytes, checksum: 025fa5a5cbc2420be7cb75fa51f61ebe (MD5) Previous issue date: 2018-07-19"]},{"key":"dc:format","label":"Dc Format","values":["application/pdf"]},{"key":"dc:title","label":"Title","values":["Nelson Oppen combination as a rewrite theory"]}]}],"canonical_facts":{"dc:contributor":["Meseguer, José"],"dc:creator":["Rodrigues, Nishant"],"dc:date":["2018-09-27T16:17:55Z","2018-07-19","2018-08"],"dc:description":["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.","Submission original under an indefinite embargo labeled 'Open Access'. The submission was exported from vireo on 2018-09-27 without embargo terms","The student, Nishant Rodrigues, accepted the attached license on 2018-07-17 at 05:43.","The student, Nishant Rodrigues, submitted this Thesis for approval on 2018-07-17 at 05:53.","This Thesis was approved for publication on 2018-07-19 at 08:53.","DSpace SAF Submission Ingestion Package generated from Vireo submission #12898 on 2018-09-27 at 10:48:54","Made available in DSpace on 2018-09-27T16:17:55Z (GMT). No. of bitstreams: 2 RODRIGUES-THESIS-2018.pdf: 160742 bytes, checksum: 883d95baf0a9eef1be969d2c42b7eef8 (MD5) LICENSE.txt: 4214 bytes, checksum: 025fa5a5cbc2420be7cb75fa51f61ebe (MD5) Previous issue date: 2018-07-19"],"dc:format":["application/pdf"],"dc:identifier":["http://hdl.handle.net/2142/101601"],"dc:language":["en"],"dc:rights":["Copyright 2018 Nishant Rodrigues"],"dc:subject":["Satisfiability Module Theories","SMT","Automated Theorem Proving","Nelson-Oppen"],"dc:title":["Nelson Oppen combination as a rewrite theory"],"dc:type":["text"],"thesis:degree_discipline":["Mathematics"],"thesis:degree_level":["Thesis"],"thesis:degree_name":["M.S."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:24:40Z"}