The CHR-based Implementation of the SCIFF Abductive System

• Autorzy: Alberti M. , Gavanelli M. , Lamma E.
• Języki publikacji: EN

Abstrakty

EN

Abduction is a form of inference that supports hypothetical reasoning and has been applied to a number of domains, such as diagnosis, planning, protocol verification. Abductive Logic Programming (ALP) is the integration of abduction in logic programming. Usually, the operational semantics of an ALP language is defined as a proof procedure. The first implementations of ALP proof-procedures were based on the meta-interpretation technique, which is flexible but limits the use of the built-in predicates of logic programming systems. Another, more recent, approach exploits theoretical results on the similarity between abducibles and constraints. With this approach, which bears the advantage of an easy integration with built-in predicates and constraints, Constraint Handling Rules has been the language of choice for the implementation of abductive proof procedures. The first CHR-based implementation mapped integrity constraints directly to CHR rules, which is an efficient solution, but prevents defined predicates from being in the body of integrity constraints and does not allow a sound treatment of negation by default. In this paper, we describe the CHR-based implementation of the SCIFF abductive proof-procedure, which follows a different approach. The SCIFF implementation maps integrity constraints to CHR constraints, and the transitions of the proof-procedure to CHR rules, making it possible to treat default negation, while retaining the other advantages of CHR-based implementations of ALP proof-procedures.

Słowa kluczowe

EN

logic programming; prediction models; mathematical proofs; default logic; semantics; verification logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2013
• Tom: Vol. 124, nr 4
• Strony: 365--381
• Opis fizyczny: Bibliogr. 40 poz., rys., tab.

Twórcy

autor

Alberti M.

• CENTRIA - DI/FCT - Universidade Nova de Lisboa, Quinta da Torre - 2829-516 Caparica, Portugal

autor

Gavanelli M.

• ENDIF - Università di Ferrara, Via Saragat, 1 - 44122 Ferrara, Italy

autor

Lamma E.

• ENDIF - Università di Ferrara, Via Saragat, 1 - 44122 Ferrara, Italy

Bibliografia

• [1] Abdennadher, S., Christiansen, H.: An Experimental CLP Platform for Integrity Constraints and Abduction, FQAS, Flexible Query Answering Systems (H. Larsen, J. Kacprzyk, S. Zadrozny, T. Andreasen, H. Christiansen, Eds.), LNCS, Springer-Verlag, Warsaw, Poland, October 25-28 2000.
• [2] Alberti, M., Bracciali, A., Chesani, F., Ciampolini, A., Endriss, U., Gavanelli, M., Guerri, A., Kakas, A., Lamma, E., Lu, W., Mancarella, P., Mello, P., Milano, M., Riguzzi, F., Sadri, F., Stathis, K., Terreni, G., Toni, F., Torroni, P., Yip, A.: Experiments With Animated Societies of Computees, Deliverable D14, SOCS Consortium, 2005, http: //lia.deis. unibo. it/SOCS/guests/publications/.
• [3] Alberti, M., Cattafi, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M., Torroni, P.: A Computational Logic Application Framework for Service Discovery and Contracting, International Journal of Web Services Research, 8(3), 2011, 1-25.
• [4] Alberti, M., Chesani, F., Daolio, D., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Specification and Verification of Agent Interaction Protocols in a Logic-based System, Scalable Computing: Practice and Experience, 8(1), 2007, 1-13, ISSN 1895-1767.
• [5] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E.: The CHR-based Implementation of a System for Generation and Confirmation of Hypotheses, Number 2005-01 in Ulmer Informatik-Berichte, 2005, ISSN 09395091.
• [6] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Montali, M.: An Abductive Framework for A-Priori Verification of Web Services, Proceedings of the Eighth Symposium on Principles and Practice of Declarative Programming, July 10-12, 2006, Venice, Italy (M. Maher, Ed.), ACM Press, New York, USA, July 2006, ISBN 1-59593-388-3.
• [7] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Compliance Verification of Agent Interaction: a Logic-based Tool, Applied Artificial Intelligence, 20(2-4), February-April 2006, 133-157.
• [8] Alberti, M., Chesani, F., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Verifiable Agent Interaction in Abductive Logic Programming: the SCIFF framework, ACM Transactions on Computational Logic, 9(4), 2008.
• [9] Alberti, M., Daolio, D., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Specification and Verification of Agent Interaction Protocols in a Logic-based System, Proceedings of the 19th Annual ACM Symposium on Applied Computing (SAC 2004). Special Track on Agents, Interactions, Mobility, and Systems (AIMS) (H. M. Haddad, A. Omicini, R. L. Wainwright, Eds.), ACM Press, Nicosia, Cyprus, March 14-17 2004.
• [10] Alberti, M., Gavanelli, M., Lamma, E.: Runtime Addition of Integrity Constraints in Abductive Logic Programs, Technical Communications of the 26th International Conference on Logic Programming (M. Hermenegildo, T. Schaub, Eds.), 7, Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, July 2010, ISBN 978-3-939897-17-0, ISSN 1868-8969.
• [11] Alberti, M., Gavanelli, M., Lamma, E.: Deon+: Abduction and Constraints for Normative Reasoning, Logic Programs, Norms and Action (A. Artikis, R. Craven, N. K. Cicekli, B. Sadighi, K. Stathis, Eds.), 7360, Springer, 2012, ISBN 978-3-642-29413-6.
• [12] Alberti, M., Gavanelli, M., Lamma, E., Mello, P., Torroni, P.: Specification and Verification of Agent Interactions using Social Integrity Constraints, Electronic Notes in Theoretical Computer Science, 85(2), 2004, 94-116, ISSN 1571-0661.
• [13] Burckert, H.: A resolution principle for constrained logics, Artificial Intelligence, 66, 1994, 235-271.
• [14] Carlsson, M., Mildner, P.: SICStus Prolog-The first 25 years, Theory and Practice of Logic Programming, 12(1-2), January 2012, 35-66.
• [15] Christiansen, H.: Executable specifications for hypothesis-based reasoning with Prolog and Constraint Handling Rules, J. Applied Logic, 7(3), 2009, 341-362.
• [16] Christiansen, H., Dahl, V.: Assumptions and Abduction in Prolog, Workshop on Multiparadigm Constraint Programming Languages (MultiCPL ’04) (S. Muiioz-Hernandez, J. M. Gomez-Perez, P. Hofstedt, Eds.), Saint-Malo, France, September 2004, Workshop notes.
• [17] Christiansen, H., Dahl, V: HYPROLOG: A New Logic Programming Language with Assumptions and Abduction., Proc. ICLP 2005 (M. Gabbrielli, G. Gupta, Eds.), 3668, Springer, 2005, ISBN 3-540-29208-X.
• [18] Denecker, M., De Schreye, D.: SLDNFA: an abductive procedure for abductive logic programs, Journal of Logic Programming, 34(2), 1998, 111-167.
• [19] Endriss, U., Mancarella, P., Sadri, F., Terreni, G., Toni, F.: The CIFF Proof Procedure for Abductive Logic Programming with Constraints, Proc. JELIA 2004 (J. J. Alferes, J. A. Leite, Eds.), 3229, Springer-Verlag, 2004, ISBN 3-540-23242-7.
• [20] Eshghi, K.: Abductive planning with the Event Calculus, Logic Programming, Proceedings of the Fifth International Conference and Symposium, Seattle, Washington, MIT Press, Cambridge, MA, 1988.
• [21] Eshghi, K., Kowalski, R. A.: Abduction compared with negation by failure, Proceedings of the 6thInterna- tional Conference on Logic Programming (G. Levi, M. Martelli, Eds.), MIT Press, 1989.
• [22] Friihwirth, T.: Theory and Practice of Constraint Handling Rules, Journal of Logic Programming, 37(1-3), October 1998, 95-138.
• [23] Fung, T. H., Kowalski, R. A.: The IFF proof procedure for abductive logic programming, Journal of Logic Programming, 33(2), November 1997, 151-165, ISSN 0743-1066.
• [24] Gavanelli, M., Alberti, M., Lamma, E.: Integration of abductive reasoning and constraint optimization in SCIFF, 25th International Conference on Logic Programming (ICLP 2009) (P. M. Hill, D. S. Warren, Eds.), 5649, Springer-Verlag, Berlin Heidelberg, 2009, ISBN 978-3-642-02845-8, ISSN 0302-9743.
• [25] Gavanelli, M., Lamma, E., Mello, P., Milano, M., Torroni, P.: Interpreting Abduction in CLP, APPIA- GULP-PRODE Joint Conference on Declarative Programming (F. Buccafurri, Ed.), Universita Mediterranea di Reggio Calabria, Reggio Calabria, Italy, September 3-5 2003.
• [26] Gavanelli, M., Rossi, F.: Constraint Logic Programming, A 25-Year Perspective on Logic Programming: Achievements of the Italian Association for Logic Programming, GULP (A. Dovier, E. Pontelli, Eds.), 6125, Springer, 2010, ISBN 978-3-642-14308-3.
• [27] Hartshorne, C., Weiss, P., Eds.: Collected Papers of Charles Sanders Peirce, 1931-1958, vol. 2, Harvards University Press, 1965.
• [28] Holzbaur, C.: OFAI clp(q,r) Manual, Austrian Research Institute for Artificial Intelligence, Vienna, 1.3.3 edition, 1995, TR-95-09.
• [29] Holzbaur, C., Friihwirth, T.: Compiling Constraint Handling Rules into Prolog with Attributed Variables, PPDP (G. Nadathur, Ed.), 1999.
• [30] Jaffar, J., Maher, M.: Constraint Logic Programming: a Survey, Journal of Logic Programming, 19-20,1994, 503-582.
• [31] Kakas, A. C., Denecker, M.: Abduction in Logic Programming, Computational Logic: Logic Programming and Beyond. Part I (A. C. Kakas, F. Sadri, Eds.), number 2407 in Lecture Notes in Artificial Intelligence, Springer-Verlag, 2002.
• [32] Kakas, A. C., Kowalski, R. A., Toni, F.: Abductive Logic Programming, Journal of Logic and Computation, 2(6), 1993,719-770.
• [33] Kakas, A. C., Michael, A., Mourlas, C.: ACLP: Abductive Constraint Logic Programming, Journal of Logic Programming, 44(1-3), July 2000, 129-177.
• [34] Kakas, A. C., vanNuffelen, B., Denecker, M.: A-System: Problem Solving through Abduction, Proc. of the Seventeenth Int. Joint Conf. on Artificial Intelligence (IJCAI-01) (B. Nebel, Ed.), 2001.
• [35] Kowalski, R., Toni, F., Wetzel, G.: Executing Suspended Logic Programs, Fundamenta Informaticae, 34, 1998, 203-224.
• [36] Mancarella, P., Terreni, G., Sadri, F., Toni, F., Endriss, U.: The CIFF proof procedure for abductive logic programming with constraints: Theory, implementation and experiments, TPLP, 9(6), 2009,691-750.
• [37] VanNuffelen, B.: Abductive Constraint Logic Programming: Implementation and Applications, Ph.D. Thesis, Katholieke Universiteit Leuven, 2004.
• [38] Schrijvers, T., Demoen, B.: The K.U. Leuven CHR system: implementation and application, Proc. CHR ’04 (T. Frhwirth, M. Meister, Eds.), Ulm, Germany, May 2004.
• [39] Wielemaker, J., Schrijvers, T., Triska, M., Lager, T.: SWI-Prolog, Theory and Practice of Logic Programming, 12(1-2), January 2012, 67-96.
• [40] Wolf, A.: Adaptive Constraint Handling with CHR in Java, Principles and Practice of Constraint Programming - CP 2001 (T. Walsh, Ed.), 2239, Springer Verlag, November 2001, ISBN 3-540-42863-1.