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). 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 θ-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.
CITATION STYLE
Di Mauro, N., Basile, T. M. A., Ferilli, S., Esposito, F., & Fanizzi, N. (2003). An exhaustive matching procedure for the improvement of learning efficiency. In Lecture Notes in Artificial Intelligence (Subseries of Lecture Notes in Computer Science) (Vol. 2835, pp. 112–129). Springer Verlag. https://doi.org/10.1007/978-3-540-39917-9_9
Mendeley helps you to discover research relevant for your work.