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 theta-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.
theta-subsumption and Resolution: A New Algorithm
FERILLI, Stefano;DI MAURO, NICOLA;BASILE, TERESA MARIA;ESPOSITO, Floriana
2003-01-01
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 theta-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.File in questo prodotto:
Non ci sono file associati a questo prodotto.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.