{"id":{"repo_id":"uiuc","oai_identifier":"oai:www.ideals.illinois.edu:2142/81950"},"canonical_url":"https://search.dev.ndltd.org/etd/uiuc/oai:www.ideals.illinois.edu:2142/81950","repository":{"repo_id":"uiuc","name":"University of Illinois - Urbana-Champaign","base_url":"https://www.ideals.illinois.edu/oai-pmh"},"display":{"title":"Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning","abstract":"This thesis investigates the problem of combining constraint reasoners. Its main goal is to establish general, possibly minimal, sets of requirements for the combination of constraint domains and reasoners. It mostly concentrates on the combination of satisfiability procedures, building on previous work by G. Nelson and D. Oppen, and by Ch. Ringeissen, but it also relates to the existing results on the combination of constraint solvers. The main theoretical results of this investigation are a number of general conditions under which it is possible to produce sound and complete combined solvers modularly. Its main practical results are an extension of the Nelson-Oppen combination method to constraint reasoners with non-disjoint constraint languages, and a novel combination method for the word problem.","abstract_html":"This thesis investigates the problem of combining constraint reasoners. Its main goal is to establish general, possibly minimal, sets of requirements for the combination of constraint domains and reasoners. It mostly concentrates on the combination of satisfiability procedures, building on previous work by G. Nelson and D. Oppen, and by Ch. Ringeissen, but it also relates to the existing results on the combination of constraint solvers. The main theoretical results of this investigation are a number of general conditions under which it is possible to produce sound and complete combined solvers modularly. Its main practical results are an extension of the Nelson-Oppen combination method to constraint reasoners with non-disjoint constraint languages, and a novel combination method for the word problem.","abstract_has_math":false,"creators":["Tinelli, Cesare"],"institution":"University of Illinois at Urbana-Champaign","degree_name":"Ph.D.","degree_level":"Dissertation","degree_discipline":"Computer Science","degree_department":null,"school":null,"contributors":["Harandi, Mehdi T."],"advisors":[],"committee_chairs":[],"committee_members":[],"year":2015,"date_issued":"2015-09-25T20:21:09Z","date_published":"2015-09-25T20:21:09Z","updated_at":"2026-07-22T22:26:17Z","subjects":["Computer Science"],"languages":["eng"],"rights":[],"rights_urls":[],"identifier_entries":[{"key":"dc:identifier","label":"Identifier","values":["(MiAaPQ)AAI9945012"],"render_values":[{"text":"(MiAaPQ)AAI9945012","href":null,"code":true}]}]},"links":{"outbound_url":"http://hdl.handle.net/2142/81950","outbound_label":"Handle","outbound_source":"dc:identifier"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor","label":"Contributor","values":["Harandi, Mehdi T."]},{"key":"dc:creator","label":"Author","values":["Tinelli, Cesare"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date","label":"Dc Date","values":["2015-09-25T20:21:09Z","10000-01-01","1999"]},{"key":"dc:type","label":"Dc Type","values":["text"]},{"key":"thesis:degree_discipline","label":"Discipline","values":["Computer Science"]},{"key":"thesis:degree_level","label":"Degree Level","values":["Dissertation"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Ph.D."]},{"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":["Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language","label":"Dc Language","values":["eng"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier","label":"Identifier","values":["http://hdl.handle.net/2142/81950","(MiAaPQ)AAI9945012"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This thesis investigates the problem of combining constraint reasoners. Its main goal is to establish general, possibly minimal, sets of requirements for the combination of constraint domains and reasoners. It mostly concentrates on the combination of satisfiability procedures, building on previous work by G. Nelson and D. Oppen, and by Ch. Ringeissen, but it also relates to the existing results on the combination of constraint solvers. The main theoretical results of this investigation are a number of general conditions under which it is possible to produce sound and complete combined solvers modularly. Its main practical results are an extension of the Nelson-Oppen combination method to constraint reasoners with non-disjoint constraint languages, and a novel combination method for the word problem.","Made available in DSpace on 2015-09-25T20:21:09Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 9945012.pdf: 9651657 bytes, checksum: 20cd2bf5ff8605495e37b51ee88aeea4 (MD5) Previous issue date: 1999","Embargo set by: Seth Robbins for item 83231 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","172 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1999."]},{"key":"dc:title","label":"Title","values":["Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning"]}]}],"canonical_facts":{"dc:contributor":["Harandi, Mehdi T."],"dc:creator":["Tinelli, Cesare"],"dc:date":["2015-09-25T20:21:09Z","10000-01-01","1999"],"dc:description":["This thesis investigates the problem of combining constraint reasoners. Its main goal is to establish general, possibly minimal, sets of requirements for the combination of constraint domains and reasoners. It mostly concentrates on the combination of satisfiability procedures, building on previous work by G. Nelson and D. Oppen, and by Ch. Ringeissen, but it also relates to the existing results on the combination of constraint solvers. The main theoretical results of this investigation are a number of general conditions under which it is possible to produce sound and complete combined solvers modularly. Its main practical results are an extension of the Nelson-Oppen combination method to constraint reasoners with non-disjoint constraint languages, and a novel combination method for the word problem.","Made available in DSpace on 2015-09-25T20:21:09Z (GMT). No. of bitstreams: 2 license.txt: 4848 bytes, checksum: 96035ab3f5e1c23cc7138a224ce498bd (MD5) 9945012.pdf: 9651657 bytes, checksum: 20cd2bf5ff8605495e37b51ee88aeea4 (MD5) Previous issue date: 1999","Embargo set by: Seth Robbins for item 83231 Lift date: Forever Reason: Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","Restricted to the U of I community idenfinitely during batch ingest of legacy ETDs","U of I Only","172 p.","Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1999."],"dc:identifier":["http://hdl.handle.net/2142/81950","(MiAaPQ)AAI9945012"],"dc:language":["eng"],"dc:subject":["Computer Science"],"dc:title":["Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning"],"dc:type":["text"],"thesis:degree_discipline":["Computer Science"],"thesis:degree_level":["Dissertation"],"thesis:degree_name":["Ph.D."],"thesis:institution_name":["University of Illinois at Urbana-Champaign"]},"updated_at":"2026-07-22T22:26:17Z"}