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).
@cite_4: Answer set programming (ASP for short) is a declarative problem solving framework that has been recently attracting the attention of researchers for its expressiveness and for its well-engineered and optimized implementations. Still, state-of-the-art answer set solvers have huge memory requirements, because the ground instantiation of the input program must be computed before the actual reasoning starts. This prevents ASP to be effective on several classes of problems. In this paper we integrate answer set generation and constraint solving to reduce the memory requirements for a class of multi-sorted logic programs with cardinality constraints. We prove some theoretical results, introduce a provably sound and complete algorithm, and report experimental results showing that our approach can solve problem instances with significantly larger domains.
@cite_12: The paper introduces a collection of knowledge representation languages, ν(C), parametrised over a class C of constraints. ν(C) is an extension of both CR-Prolog and CASP allowing the separation of a program into two parts: a regular program of CR-Prolog and a collection of denials whose bodies contain constraints from C with variables ranging over large domains. We study an instance AC0 from this family where C is a collection of constraints of the form X - Y > K. We give brief implementation details of an algorithm computing the answer sets of programs of AC0 which does not ground constraint variables and tightly couples the "classical" ASP algorithm with an algorithm checking consistency of difference constraints. We present several examples to show the methodology of representing knowledge in AC0. The work makes it possible to solve problems which could not be solved by pure ASP or constraint solvers.
As expected (and as shown in Section below), delegating the checks to a finite-domain constraint solver results in performances an order of magnitude faster than any answer set solver. Note that the ASP community is aware of this problem and recently some work has been initiated on integrating ASP with constraint solvers, in an effort to reduce the grounding size and speed computation (e.g., @cite_4 @cite_12 ), but for limited forms of constraints and restricted combinations of logic programs and constraints.