Deduction search with generalized terms

Abstract

An efficient method for generating derivable objects in calculuses over terms is proposed. The method is based on the fact that inference rules may require only partial information about their premises. It means that we can apply an inference rule not to single terms (or n-tuples of terms, if the rule has n premises) but to sets of terms (sets of n-tuples) whose elements are equivalent to each other with respect to the rule. This may reduce considerably the running time of deduction search algorithms. In some cases this approach even turns infinite search space into finite one.

The proposed method is applicable to a wide range of calculuses. In particular, this method can be used for optimization of logic program execution.