Previous: TR 91-09 Next: TR 91-15

Intellektik: Technical report 91-11

A Generalized Factorization Rule Based on the Introduction of Skolem Terms

Uwe Egly

In this paper, we describe a factorization rule which is based on the introduction of Skolem terms in order to generalize non-unifiable terms. Clauses of the form p(x,t1) or p(y,t2) are factorized to p(x,m) where t1, t2 are ground terms and m is a new constant not occuring in the Herbrand universe of the original clause set. A refutation of p(x,m) implies a refutation of p(x,t1) or p(y,t2) but not vice versa. Therefore, the rule is sound but not complete. We extend this factorization rule in several ways and show that the application of such rules may increase the preformance of automated theorem provers dramatically.

Full Paper: Compressed postscript Compressed DVI

BibTeX entry