Computing Abduction in Semantic Tableaux

Abstract

Abstract. The aim o/ this paper is to propose a way to extend the framework o/ semantic tableaux in order ta compute several /orma o/ abductive explanations: atomic, conjunctive and in disjunctive formo Our /ocus is on computing consistenf. explanations. 'fflat is, lormulas which satisfy the emailment and the consistency condition 01 the standard logical lormulation 01 abduction. Our stmtegy lor computing abductive explanations avoids the constroction 01 inconsistencies and it is done in a compositional lashion¡ abductive explanations with complez /orma are corutrocted fromsimpler ones. This allows us to identify special C41es, lor ezample that in which there are no consistent atomic explanations whatSDever.