Dissertation

Cesare Tinelli, Combining Satisfiability Procedures for Automated Deduction and Constraint-based Reasoning,
Department of Computer Science, University of Illinois at Urbana-Champaign,
May 1999.
(revised version)

Committee

Mehdi Harandi (chair), Nachum Dershowitz, Ward Henson, Uday Reddy.

Description

The main goal of this work was devising general methods for combining decision procedures for Constraint-based Reasoning. Constraint-based Reasoning is a deductive paradigm that combines the versatility of general-purpose reasoning with the performance of specialized constraint solving. Its full-scale applicability is presently hindered by the difficulty of integrating several constraint solvers in a modular way into one general-purpose reasoner.

Building automated reasoners from smaller building blocks is harder than in the case of conventional software because any modular development technique has to be worked out at a model-theoretic level first. In the case of constraint solvers, since each solver decides satisfiability with respect to a specific constraint theory, to combine solvers first of all means to combine their theories.

The known methods in the field have been essentially limited to component procedures whose underlying theories are disjoint. Using a novel model-theoretic approach, I have instead developed a general combination framework which includes several of the known combination results and methods and extends them significantly to the case of non-disjoint component theories.

This dissertation originated from the work I did for my Master's thesis, where I integrated a well-know combination procedure by Nelson and Oppen into the Constrain Logic Programming scheme by Jaffar and Lassez. Part of the work of the dissertation was carried over in the context of two parallel collaborations with Franz Baader of the Technical University of Aachen, Germany, and Christophe Ringeissen of CNRS/INRIA, France. The work with them is described in a number of technical reports and refereed publications. See my publications page for more details and online versions of the papers.


Last Updated: October 1999