Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning

172 p.Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1999.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.U of I OnlyRestricted to the U of I community idenfinitely during batch ingest of legacy ETD