Abstract

Theorem provers are systems that automate the process of inferring new facts from declarative knowledge expressed in a formal logic. For many restricted logical theories, specialized decision procedures exist that can be used to formally establish a theorem in that theory. The combination problem addresses the issue of integrating two decision procedures so that the resulting procedure handles a larger class of logical theories. A powerful idea frequently used in designing combination procedures is that of variable abstraction. This refers to the process of introducing new variables (and corresponding definitions) so that terms consisting of symbols from two different logical theories can be replaced by terms consisting of symbols from one of the two theories (sharing only the new symbols). We view the congruence closure problem as a combination problem and apply the variable abstraction technique to it to obtain the notion of an abstract congruence closure. We present logical inference rules to construct congruence closure in $O(n\log(n))$ time. The resulting decision procedure can be extended to handle additional associative-commutative function symbols. If we consider the rewrite relation, rather than the congruence relation, we get the notion of a tree automata and an abstract rewrite closure. The combination of congruence closure and rewrite closure can be used to solve a long-standing open problem in term rewriting.

Dr. Ashish Tiwari s currently employed as a Computer Scientist with the Formal Methods Group of the Computer Science Laboratory at SRI International, CA. He is currently working on formal methods for analysis for hybrid and discrete systems. Some of his other research interests are in term rewriting, saturation based theorem proving, and decision procedures. He got his PhD in Computer Science from the State University of New York at Stony Brook in 2000 and his Bachelors degree in Computer Science from the Indian Institute of Technology, Kanpur in 1995.