Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning
Tinelli, Cesare
This item is only available for download by members of the University of Illinois community. Students, faculty, and staff at the U of I may log in with your NetID and password to view the item. If you are trying to access an Illinois-restricted dissertation or thesis, you can request a copy through your library's Inter-Library Loan office or purchase a copy directly from ProQuest.
Permalink
https://hdl.handle.net/2142/81950
Description
Title
Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning
Author(s)
Tinelli, Cesare
Issue Date
1999
Doctoral Committee Chair(s)
Harandi, Mehdi T.
Department of Study
Computer Science
Discipline
Computer Science
Degree Granting Institution
University of Illinois at Urbana-Champaign
Degree Name
Ph.D.
Degree Level
Dissertation
Keyword(s)
Computer Science
Language
eng
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.
Use this login method if you
don't
have an
@illinois.edu
email address.
(Oops, I do have one)
IDEALS migrated to a new platform on June 23, 2022. If you created
your account prior to this date, you will have to reset your password
using the forgot-password link below.
