The CIFF Proof Procedure for Abductive Logic Programming

Since 2006, CIFF is maintained by Giacomo Terreni; see his website for the latest developments.

This page provides access to an implementation of the CIFF proof procedure for abductive logic programming with constraints, which is both an extension and a refinement of the IFF proof procedure proposed by Fung and Kowalski.

Download CIFF 3.0 now!

Previous versions of CIFF are also available. Note that, because of the specific constraint solver used, the program will only run under Sicstus Prolog. A number of example files are available here.

Related papers:

U. Endriss, P. Mancarella, F. Sadri, G. Terreni, and F. Toni. The CIFF Proof Procedure for Abductive Logic Programming with Constraints, In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA-2004), Springer-Verlag, September 2004.
[This is the main reference paper on CIFF.]
U. Endriss, P. Mancarella, F. Sadri, G. Terreni, and F. Toni. The CIFF Proof Procedure: Definition and Soundness Results, Technical Report 2004/2, Department of Computing, Imperial College London, May 2004.
[This is an extended version of the previous paper, including full proofs for the soundness results.]
U. Endriss, P. Mancarella, F. Sadri, G. Terreni, and F. Toni. Abductive Logic Programming with CIFF, In B. Bennett, editor, Proceedings of the 11th Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice (ARW-2004), University of Leeds, March 2004. Extended Abstract.
[This is a short paper giving an overview of CIFF and its implementation.]
U. Endriss, M. Hatzitaskos, P. Mancarella, F. Sadri, G. Terreni, and F. Toni. Refinements of the CIFF Procedure, In A. Bundy and J. Fleuriot, editors, Proceedings of the 12th Workshop on Automated Reasoning, Bridging the Gap between Theory and Practice (ARW-2005), University of Edinburgh, July 2005. Extended Abstract.
[This is a short paper describing the latest refinements of CIFF (in particular the integration of negation-as-failure).]
U. Endriss, P. Mancarella, F. Sadri, G. Terreni, and F. Toni. Abductive Logic Programming with CIFF: Implementation and Applications, In Proceedings of Convegno Italiano di Logica Computazionale (CILC-2004) , University of Parma, June 2004.
[This paper describes the application of CIFF to planning and provides some details on the implementation.]
U. Endriss, P. Mancarella, F. Sadri, G. Terreni, and F. Toni. Abductive Logic Programming with CIFF: System Description, In Proceedings of the 9th European Conference on Logics in Artificial Intelligence (JELIA-2004), Springer-Verlag, September 2004.
[This is a short paper describing the implementation.]
U. Endriss. Implementing the CIFF Procedure, Preliminary and incomplete draft, December 2003.
[This paper gives some additional details on the implementation of CIFF and explains how to use it.]
T. H. Fung and R. A. Kowalski. The IFF Proof Procedure for Abductive Logic Programming. Journal of Logic Programming, 33(2):151-165, 1997.

This research has been supported by the European Union as part of the SOCS project (IST-2001-32530). In case of problems, questions, or suggestions, please contact Ulle Endriss (ue@doc.ic.ac.uk).