Completeness for cut-based abduction

被引：1

作者：

Arruda, Alexandre Matos ^{[1
]}

Finger, Marcelo ^{[1
]}

机构：

[1] Univ Sao Paulo, Dept Comp Sci, Inst Math & Stat, Sao Paulo, Brazil

来源：

LOGIC JOURNAL OF THE IGPL | 2014年 / 22卷 / 02期

基金：

巴西圣保罗研究基金会;

关键词：

Abduction; first-order abduction; cut-based abduction; tableaux; propositional tableaux; first-order tableaux; KE-tableaux;

D O I：

10.1093/jigpal/jzt028

中图分类号：

O29 [应用数学];

学科分类号：

070104 ;

摘要：

In traditional abduction methods it is assumed that the goal data has not yet been explained. In first-order logic (FOL) such precondition is, in general, undecidable. To avoid this problem, it was presented in D'Agostino, Finger and Gabbay (2008, Logic J. of the IGPL, 16, 537-560) a first-order cut-based abduction method which has as underlying inference system the KE-tableaux. Such inference system is non-analytical and the method presented in D'Agostino, Finger and Gabbay (2008, Logic J. of the IGPL, 16, 537-560) generalizes the traditional abduction avoiding the undecidable precondition; its correctness was demonstrated. Here we will show the completeness of the method for both propositional and first-order logic.

引用

页码：286 / 296

页数：11