The CIFF Proof Procedure for Abductive Logic Programming with Constraints: Theory, Implementation and Experiments

TL;DR

This paper introduces the CIFF proof procedure for abductive logic programming with constraints, extending previous methods by relaxing restrictions and integrating a constraint solver, with implementation and experimental evaluation.

Contribution

It presents the CIFF proof procedure, extending IFF by relaxing variable restrictions and incorporating constraint solving, along with system implementation and comparative analysis.

Findings

Proved the correctness of CIFF

Compared CIFF with other abductive systems and answer set solvers

Demonstrated applications of CIFF in programming tasks

Abstract

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).