θ-subsumption and resolution: A new algorithm

Abstract

Efficiency of the first-order logic proof procedure is a major issue when deduction systems are to be used in real environments, both on their own and as a component of larger systems (e.g., learning systems). This paper proposes a new θ-subsumption algorithm that is able to return the set of all substitutions by which such a relation holds between two clauses without performing backtracking. Differently from others proposed in the literature, it can be extended to perform resolution, also in theories containing recursive clauses.