Towards automated first-order abduction: the cut-based approach

Autor(es)

Finger, Marcelo

• Tipo de documento: Artigo Científico
• Fonte: LOGIC JOURNAL OF THE IGPL; v. 20, n. 2, p. 18-pg., 2012-04-01.

Resumo

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. (AU)

• Processo FAPESP: 08/03995-5 - LOGPROB: lógica probabilística - fundamentos e aplicações computacionais
• Beneficiário: Marcelo Finger
• Modalidade de apoio: Auxílio à Pesquisa - Temático