News Archives

Combining Decision Procedures for Sorted Theories

April 19, 2005

  • Date: Tuesday, April 19, 2005 
  • Time: 11:00 a.m. 
  • Place: Woodward 149

Dr. Calgero Zarba <[email protected]> 
Department of Computer Science University of New Mexico

The Nelson-Oppen combination method combines decision procedures for theories satisfying certain conditions into a decision procedure for their union. While the method is known to be correct in the setting of unsorted first-order logic, some current implementations of it appear in tools that use a sorted input language. Until 2004, however, there have been no theoretical results on the correctness of the method in a sorted setting, nor is it obvious that the method in fact lifts as is to logics with sorts.

To bridge this gap between the existing theoretical results and the current implementations, we extend the Nelson-Oppen method to (order-)sorted logic and prove it correct under conditions similar to the original ones. From a theoretical point of view, the extension is relevant because it provides a rigorous foundation for the application of the method in a sorted setting.

From a practical point of view, the extension has the considerable added benefits that in a sorted setting the method’s preconditions become easier to satisfy in practice, and the method’s nondeterminism is generally reduced.

* Based on a joint work with Cesare Tinelli (University of Iowa).