Artículos de revistas
Towards automated first-order abduction: the cut-based approach
LOGIC JOURNAL OF THE IGPL, OXFORD, v. 20, n. 2, Special Issue, supl. 1, Part 1, pp. 370-387, APR, 2012
Traditional abduction imposes as a precondition the restriction that the background information may not derive the goal data. In first-order logic such precondition is, in general, undecidable. To avoid such problem, we present a first-order cut-based abduction method, which has KE-tableaux as its underlying inference system. This inference system allows for the automation of non-analytic proofs in a tableau setting, which permits a generalization of traditional abduction that avoids the undecidable precondition problem. After demonstrating the correctness of the method, we show how this method can be dynamically iterated in a process that leads to the construction of non-analytic first-order proofs and, in some terminating cases, to refutations as well.