Combining Satisfiability Procedures for Automated Deduction and Constraint -Based Reasoning

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.

Name thesis:degree_name

Ph.D.

Level thesis:degree_level

Dissertation

Discipline thesis:degree_discipline

Computer Science

Grantor

University of Illinois at Urbana-Champaign

Year dc:date

2015

Author dc:creator

• Tinelli, Cesare

Contributors dc:contributor

• Harandi, Mehdi T.

• Computer Science

Language dc:language

eng

Identifier

(MiAaPQ)AAI9945012

OAI identifier oai:identifier

oai:www.ideals.illinois.edu:2142/81950