Reducing search space in solving higher-order equations

Tetsuo Ida

Mircea Marin

Taro Suzuki

pp. 19-30

in: Setsuo Arikawa, Ayumi Shinohara (eds), Progress in discovery science, Berlin, Springer, 2002

Abstract

We describe the results of our investigation of equational problem solving in higher-order setting. The main problem is identified to be that of reducing the search space of higher-order lazy narrowing calculi, namely how to reduce the search space without losing the completeness of the calculi. We present a higher-order calculus HOLN₀ as a system of inference rules and discuss various refinements that enable the reduction of the search space by eliminating some sources of nondeterminism inherent in the calculus.