Algorithmic aspects of symbolic computation with associativity and commutativity
Ta Chen · 1996
This dissertation discusses the design and implementation of efficient algorithms for fundamental operations that typically arise in symbolic computation with associativity and commutativity (AC). We first focus on developing an AC term matching algorithm. Use of discrimination nets for many-to-one pattern matching has been shown to dramatically improve the performance of the Knuth-Bendix completion procedure used in rewriting. Many important applications of rewriting require AC function symbols and it is therefore quite natural to expect performance gains by using similar techniques for AC-completion. In this dissertation we propose such a technique, called AC-discrimination net, that is a natural generalization of the standard discrimination net. Moreover we show how AC-discrimination nets can be augmented so as to further improve the performance of AC-matching on problems that are typically seen in practice. We also discuss the integration of such discrimination nets into an actual equational theorem prover and report on corresponding experiments. The general AC-matching problem is known to be NP-complete, but can be solved in polynomial time if the given terms are linear. We therefore have implemented a two-stage matching procedure. First we check whether a match exists for the linearized versions of the given terms. If a match for the linearized terms does exist, we then determine whether there is also a match for the original, non-linear terms. Our experimental results indicate that this approach works very well in theorem proving. Term-matching usually occurs in the larger context of normalizing a given input term s. In such a context, identifying redexes, called subterm matching in s is a crucial step toward efficient normalization of s. In the literature, there have been two approaches for non-AC terms, top-down and bottom-up, depending on how symbols in s are examined. In this dissertation, we extend both approaches to handle AC-terms. We also provide experimental results of AC-subterm matching, both top-down and bottom-up, and compare their performance with that of AC-discrimination nets. Finally, we discuss clause subsumption, which is an important operation in resolution-based theorem provers. Subsumption is a special case of ACI-matching, where clauses are viewed as terms and only the top symbols are allowed to be ACI. In this dissertation, we investigate the possibility of improving existing subsumption algorithms and offer a better upper bound on time complexity through a considerably simpler analysis.