Files in this item



application/pdf9945012.pdf (10MB)Restricted to U of Illinois
(no description provided)PDF


Title:Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning
Author(s):Tinelli, Cesare
Doctoral Committee Chair(s):Harandi, Mehdi T.
Department / Program:Computer Science
Discipline:Computer Science
Degree Granting Institution:University of Illinois at Urbana-Champaign
Subject(s):Computer Science
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.
Issue Date:1999
Description:172 p.
Thesis (Ph.D.)--University of Illinois at Urbana-Champaign, 1999.
Other Identifier(s):(MiAaPQ)AAI9945012
Date Available in IDEALS:2015-09-25
Date Deposited:1999

This item appears in the following Collection(s)

Item Statistics