An Exhaustive Matching Procedure for the Improvement of Learning Efficiency

Efficiency of the first-order logic proof procedure is a major issue when deduction systems axe to be used in real environments, both on their own and as a component of larger systems (e.g., learning systems). Hence, the need of techniques that can speed up such a process. This paper proposes a new algorithm for matching first-order logic descriptions under theta-subsumption that is able to return the set of all substitutions by which such a relation holds between two clauses, and shows experimental results in support of its performance.