Order-Sorted Congruence Closure
Jean H. Gallier, Tomás Isakowitz · ScholarlyCommons (University of Pennsylvania) · 1988
In this paper, an algorithm for testing the unsatisfiability of a set of ground order-sorted equational Horn clauses (for coherent signatures) is presented. This result follows from the fact that the concept of congruence closure extends to finite sets of ground order-sorted equational Horn clauses. We show how to compute the order-sorted congruence closure and obtain an algorithm running in O(η2).