On High-Level Inferencing and the Variable Binding Problem in Connectionist Networks

Abstract

We present a connectionist inference system for Horn logic. The system is based on a unification algorithm for first-order terms and uses Bibel’s connection method. It is restricted in that only one instance of each clause may be used in a proof. But there are no restrictions concerning function symbols or the occurrence of variables. In particular, the inference system handles n-ary function and predicate symbols and multiple occurrences of variables even if these variables are not introduced in the conclusion of a rule. The deductive system has more expressive power than the connectionist high-level inference systems we are aware of. This is elaborated by showing how certain additional restrictions imposed on our system lead to the known inference systems. These additional restrictions are ultimately linked to the way how the variable binding problem is solved.