A specialized ATMS for equivalence relations

Graduation date: 1989A specialized ATMS for efficiently computing equivalence relations in multiple contexts is introduced. This specialized ATMS overcomes the problems with existing solutions to reasoning with equivalence relations. The most direct implementation of an equivalence relation in the ATMS-encoding the reflexive, transitive, and symmetric rules in the consumer architecture-produces redundant equality derivations and requires Θ(n³) label update attempts (where n is the number of terms in the equivalence class). An alternative implementation is one that employs simple equivalence classes. However, this solution is unacceptable, since the number of classes grows exponentially with the number of distinct assumptions. The specialized ATMS presented here produces no redundant equality derivations, requires only Θ(n²) label update attempts, and is most efficient when there are many distinct assumptions and few nogoods. This is achieved by exploiting a special relationship that holds among the labels of the equality assertions because of transitivity. The standard dependency structure construction and traversal is replaced by a single pass over each label in a particular kind of equivalence class. The specialized ATMS has been implemented as part of the logic programming language FORLOG