Computational problems in equational theorem proving
Jonathan Stillman · 1989
We study computational aspects of equational reasoning related to the complexity of determining whether a term rewriting system is terminating, and to automated theorem proving in first-order logic. Detection of homeomorphic embedding can be used as an aid in detecting potential nontermination of rewriting. We show that, given a pair of ground terms, the problem of determining the existence of homeomorphic embedding of one term into another is NP-complete when functions may be associative and commutative, solving an open problem posed in (46). We present polynomial algorithms for a number of restricted cases. We show that determining whether there exists a matching that results in a homeomorphic embedding of one term into another is NP-complete. We demonstrate a polynomial algorithm for detecting whether, given two terms s and t, s is semi-unifiable with t. This procedure is also useful for detecting nontermination of rewriting. We show that it is undecidable whether the Knuth-Bendix completion procedure generates a crossed pair of rules. This resolves an open question posed in (23), where the applicability of such a test to detection of divergence is discussed. Our proof technique generalizes: we provide a simple proof that the universal matching problem is undecidable for regular canonical theories, a result first proved in (21). We also prove that the universal unification problem is undecidable for permutative canonical theories, and discuss other generalizations. We move to an examination of the use of equational methods for reasoning in propositional calculus, which can be expressed in terms of computing the Grobner Basis of a set of polynomials over a Boolean polynomial ring. We show that exponential time and space are necessary and sufficient for computing such a basis. We show that the exponential lower bound holds even when the original basis corresponds to a set of propositional Horn clauses. We show that even under very limiting restrictions on the input form of a set of first-order polynomials it remains undecidable whether the set is consistent. We examine the effect of limiting inference to idempotent inference and reduction. We show that it is undecidable whether this procedure will terminate, even when the system is guaranteed to be noetherian. We discuss experimental results based on two strategies based upon these restrictions.