We present the CIFF proof procedure for abductive logic programming with constraints, and we prove its correctness. CIFF is an extension of the IFF proof procedure for abductive logic programming, relaxing the original restrictions over variable quantification (allowedness conditions) and incorporating a constraint solver to deal with numerical constraints as in constraint logic programming. Finally, we describe the CIFF system, comparing it with state of the art abductive systems and answer set solvers and showing how to use it to program some applications. (To appear in Theory and Practice of Logic Programming - TPLP).
The , as remarked in @cite_16 , is a combination of three existing abductive proof procedures, namely the IFF proof procedure @cite_7 , the ACLP proof procedure @cite_25 and, most importantly, the SLDNFA proof procedure @cite_59 , of which the is a direct descendant. The is the state-of-the-art of abductive logic programming with constraints, borrowing the most interesting features from the above cited proof procedures. In Section we give a detailed comparison between CIFF and the .
@cite_59 @cite_16 @cite_25 @cite_7
2022472812 190622319 2071787143 2078139775
Abstract We present SLDNFA, an extension of SLDNF resolution for abductive reasoning on abductive logic programs. SLDNFA solves the floundering abduction problem: nonground abductive atoms can be selected. SLDNFA also provides a partial solution for the floundering negation problem. Different abductive answers can be derived from an SLDNFA refutation; these answers provide different compromises between generality and comprehensibility. Two extensions of SLDNFA are proposed that satisfy stronger completeness results. The soundness of SLDNFA and its extensions is proved. Their completeness for minimal solutions with respect to implication, cardinality, and set inclusion is investigated. The formalization of SLDNFA presented here is an update of an older version and does not rely on skolemization of abductive atoms. Abstract We propose an extension of the SLDNF proof procedure for checking integrity constraints in deductive databases. To achieve the effect of the simplification methods investigated by Nicolas [1982], Lloyd, Sonenberg, and Topor [1986], and Decker [1986], we use clauses corresponding to the updates as top clauses for the search space. This builds in the assumption that the database satisfied its integrity constraints prior to the transaction, and that, therefore, any violation of the constraints in the updated database must involve at least one of the updates in the transaction. Different simplification methods can be simulated by different strategies for literal selection and search. The SLDNF proof procedure needs to be extended to use as top clause any arbitrary deductive rule, denial, or negated fact, to incorporate inference rules for reasoning about implicit deletions resulting from other deletions and additions, and to allow an extended resolution step for reasoning forward from negated facts. Abstract In this paper, we outline a proof procedure which combines reasoning with defined predicates together with reasoning with undefined, abducible , predicates. Defined predicates are defined in if-and-only-if form. Abducible predicates are constrained by means of integrity constraints. Given an initial query, the task of the proof procedure is to construct a definition of the abducible predicates and a substitution for the variables in the query, such that both the resulting instance of the query and the integrity constraints are implied by the extended set of definitions. The iff proof procedure can be regarded as a hybrid of the proof procedure of and the SLDNFA procedure of Denecker and De Schreye. It consists of a number of inference rules which, starting from the initial query, rewrite a formula into an equivalent formula. These rules are: 1) unfolding , which replaces an atom by its definition; 2) propagation , which resolves an atom with an implication; 3) splitting , which uses distributivity to represent a goal as a disjunction of conjunctions; 4) case analysis for an equality X = t in the conditions of an implication, which considers the two cases X = t and X ≠ t ; 5) factoring of two abducible atoms, which considers the two cases, where the atoms are identical and where they are different, 6) rewrite rules for equality , which simulate the unification algorithm; and 7) logical simplifications , such as A ∧ false ↔ false . The proof procedure is both sound and complete relative to the three-valued completion semantics. These soundness and completeness results improve previous results obtained for other proof procedures. Abstract This paper presents the framework of Abductive Constraint Logic Programming (ACLP), which integrates Abductive Logic Programming (ALP) and Constraint Logic Programming (CLP). In ACLP, the task of abduction is supported and enhanced by its non-trivial integration with constraint solving. This integration of constraint solving into abductive reasoning facilitates a general form of constructive abduction and enables the application of abduction to computationally demanding problems. The paper studies the formal declarative and operational semantics of the ACLP framework together with its application to various problems. The general characteristics of the computation of ACLP and of its application to problems are also discussed. Empirical results based on an implementation of the ACLP framework on top of the CLP language of ECLiPSe show that ACLP is computationally viable, with performance comparable to the underlying CLP framework on which it is built. In addition, our experiments show the natural ability for ACLP to accommodate easily and in a robust way new or changing requirements of the original problem. ACLP thus combines the advantages of modularity and flexibility of the high-level representation afforded by abduction together with the computational effectiveness of low-level specialised constraint solving.