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).
There is a huge literature on abductive logic programming with and without constraints, see for example @cite_14 @cite_34 @cite_15 @cite_57 @cite_18 @cite_25 @cite_0 @cite_23 @cite_48 @cite_59 @cite_16 @cite_19 @cite_7 @cite_26 @cite_68 @cite_8 @cite_54 @cite_43 @cite_47 . The closest systems to CIFF are the @cite_16 and @cite_28 . The latter has also been developed as an extension of the IFF proof procedure to handle numerical constraints as in CLP, but with focus on the specification and verification of interactions in open agent societies. The main features of are the support of dynamical happening of events during computations, universally quantified variables in abducibles, the concept of fulfilment and violation of expectations, given a set of events, and integrity constraints of a specialised form which requires to include in their body at least one specific social construct (an event or an expectation). Instead, CIFF is intended as a general purpose abductive proof procedure, keeping the spirit of the original IFF proof procedure and conservatively adding numerical constraints.
@cite_54 @cite_43 @cite_15 @cite_18 @cite_8 @cite_48 @cite_23 @cite_68 @cite_26 @cite_7 @cite_28 @cite_57 @cite_19 @cite_16 @cite_34 @cite_25 @cite_14 @cite_0 @cite_59 @cite_47
176609766 1531065626 2071787143 2078139775
Horn clause logic programming can be extended to include abduction with integrity constraints. In the resulting extension of logic programming, negation by failure can be simulated by making negative conditions abducible and by imposing appropriate denials and disjunctions as integrity constraints. This gives an alternative semantics for negation by failure, which generalises the stable model semantics of negation by failure. The abductive extension of logic programming extends negation by failure in three ways: (1) computation can be perfonned in alternative minimal models, (2) positive as well as negative conditions can be made abducible, and (3) other integrity constraints can also be accommodated. * This paper was written while the first author was at Imperial College. 235 Introduction The tenn "abduction" was introduced by the philosopher Charles Peirce [1931] to refer to a particular kind of hypothetical reasoning. In the simplest case, it has the fonn: From A and A fB infer B as a possible "explanation" of A. Abduction has been given prominence in Charniak and McDennot's [1985] "Introduction to Artificial Intelligence", where it has been applied to expert systems and story comprehension. Independently, several authors have developed deductive techniques to drive the generation of abductive hypotheses. Cox and Pietrzykowski [1986] construct hypotheses from the "dead ends" of linear resolution proofs. Finger and Genesereth [1985] generate "deductive solutions to design problems" using the "residue" left behind in resolution proofs. Poole, Goebel and Aleliunas [1987] also use linear resolution to generate hypotheses. All impose the restriction that hypotheses should be consistent with the "knowledge base". Abduction is a fonn of non-monotonic reasoning, because hypotheses which are consistent with one state of a knowledge base may become inconSistent when new knowledge is added. Poole [1988] argues that abduction is preferable to noh-monotonic logics for default reasoning. In this view, defaults are hypotheses fonnulated within classical logic rather than conclusions derived withln some fonn of non-monotonic logic. The similarity between abduction and default reasoning was also pointed out in [Kowalski, 1979]. In this paper we show how abduction can be integrated with logic programming, and we concentrate on the use of abduction to generalise negation by failure. Conditional Answers Compared with Abduction In the simplest case, a logic program consists of a set of Horn Clauses, which are used backward to_reduce goals to sub goals. The initial goal is solved when there are no subgollls left; Recent work has suggested abductive logic programming as a suitable formalism to represent active databases and intelligent agents. In particular, abducibles in abductive logic programs can be used to represent actions, and integrity constaints in abductive logic programs can be used to represent active rules of the kind encountered in active databases and reactive rules incorporating reactive behaviour in agents. One would expect that, in this approach, abductive proof procedures could provide the engine underlying active database management systems and the behaviour of agents. We analyse existing abductive proof procedures and argue that they are inadequate in handling these applications. The inadequacy is due to the inappropriate treatment of negative literals in integrity constraints. We propose a new abductive proof procedure and give examples of how this proof procedure can be used to achieve active behaviour in (deductive) databases and reactivity in agents. Finally, we prove some soundness and completeness results for the new proof procedure. 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.