Intellektik: Technical report 91-11
A Generalized Factorization Rule Based on the Introduction of Skolem Terms
In this paper, we describe a factorization rule which is based on
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