Recent News
Inaugural School of Engineering Teaching Innovation Fellows selected
February 2, 2024
UNM computer scientist wins NSF CAREER Award to optimize supercomputer performance
February 1, 2024
Hand and Machine Lab’s Experimental Clay Exhibition closing celebration Nov. 17
November 15, 2023
Moses selected as special assistant to the dean for educational initiatives
October 3, 2023
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 <zarba@cs.unm.edu>
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).