The-CIFF-Proof-Procedure-for-Abductive-Logic-Programming-with-Constraints.pdf
《The-CIFF-Proof-Procedure-for-Abductive-Logic-Programming-with-Constraints.pdf》由会员分享,可在线阅读,更多相关《The-CIFF-Proof-Procedure-for-Abductive-Logic-Programming-with-Constraints.pdf(13页珍藏版)》请在三一文库上搜索。
1、The CIFF Proof Procedure for Abductive Logic Programming with Constraints U. Endriss1, P. Mancarella2, F. Sadri1, G. Terreni2, and F. Toni1,2 1 Department of Computing, Imperial College London Email: ue,fs,ftdoc.ic.ac.uk 2 Dipartimento di Informatica, Universit a di Pisa Email: paolo,terreni,tonidi.
2、unipi.it Abstract. We introduce a new proof procedure for abductive logic pro- gramming and present two soundness results. Our procedure extends that of Fung and Kowalski by integrating abductive reasoning with constraint solving and by relaxing the restrictions on allowed inputs for which the proce
3、dure can operate correctly. An implementation of our proof pro- cedure is available and has been applied successfully in the context of multiagent systems. 1Introduction Abduction has found broad application as a tool for hypothetical reasoning with incomplete knowledge, which can be handled by labe
4、lling some pieces of informa- tion as abducibles, i.e. as possible hypotheses that can be assumed to hold, pro- vided that they are consistent with the given knowledge base. Abductive Logic Programming (ALP) combines abduction with logic programming enriched by integrity constraints to further restr
5、ict the range of possible hypotheses. Im- portant applications of ALP include planning 10, requirements specifi cation analysis 8, and agent communication 9. In recent years, a variety of proof procedures for ALP have been proposed, including the IFF procedure of Fung and Kowalski 4. Here, we extend
6、 this procedure in two ways, namely (1) by integrating abductive reasoning with constraint solving (in the sense of CLP, not to be confused with integrity constraints), and (2) by relaxing the allowedness conditions given in 4 to be able to handle a wider class of problems. Our interest in extending
7、 IFF in this manner stems from applications devel- oped in the SOCS project, which investigates the use of computational logic- based techniques in the context of multiagent systems for global computing. In particular, we use ALP extended with constraint solving to give computational models for an a
8、gents planning, reactivity and temporal reasoning capabilities 5. We found that our requirements for these applications go beyond available state- of-the-art ALP proof procedures. While ACLP 6, for instance, permits the use of constraint predicates (unlike IFF), its syntax for integrity constraints
9、is too restrictive to express the planning knowledge bases (using a variant of the abduc- tive event calculus 10) used in SOCS. In addition, many procedures put strong, sometimes unnecessary, restrictions on the use of variables. The procedure pro- posed in this paper, which we call CIFF, manages to
10、 overcome these restrictions to a degree that has allowed us to apply it successfully to a wide range of prob- lems. We have implemented CIFF in Prolog;3the system forms an integral part of the PROSOCS platform for programming agents in computational logic 11. In the next section we are going to set
11、 out the ALP framework used in this paper and discuss the notion of allowedness. Section 3 then specifi es the CIFF proof procedure which we propose as a suitable reasoning engine for this frame- work. Two soundness results for CIFF are presented in Section 4 and Section 5 concludes. An extended ver
12、sion of this paper that, in particular, contains detailed proofs of our results is available as a technical report 3. 2Abductive Logic Programming with Constraints We use classical fi rst-order logic, enriched with a number of special predicate symbols with a fi xed semantics, namely the equality sy
13、mbol =, which is used to represent the unifi ability of terms (i.e. as in standard logic programming), and a number of constraint predicates. We assume the availability of a sound and complete constraint solver for this constraint language. In principle, the exact specifi cation of the constraint la
14、nguage is independent from the defi nition of the CIFF procedure, because we are going to use the constraint solver as a black box component.4However, the constraint language has to include a relation symbol for equality (we are going to write t1=ct2) and it must be closed under complements. In gene
15、ral, the complement of a constraint Con will be denoted as Con (but we are going to write t16=ct2for the complement of t1=ct2). The range of admissible arguments to constraint predicates again depends on the specifi cs of the chosen constraint solver. A typical choice for a constraint system would b
16、e an arithmetic constraint solver over integers providing predicates such as and and allowing for terms constructed from variables, integers and function symbols representing operations such as addition and multiplication. Abductive logic programs.An abductive logic program is a pair hTh,ICi consist
17、ing of a theory Th and a fi nite set of integrity constraints IC. We present theories as sets of so-called iff -defi nitions: p(X1,.,Xk) D1 Dn The predicate symbol p must not be a special predicate (constraints, =, and ) and there can be at most one iff -defi nition for every predicate symbol. Each
18、of the disjuncts Diis a conjunction of literals. Negative literals are written as implications (e.g. q(X,Y ) ). The variables X1,.,Xkare implicitly univer- sally quantifi ed with the scope being the entire defi nition. Any other variable is implicitly existentially quantifi ed, with the scope being
19、the disjunct in which it 3 The CIFF system is available at http:/www.doc.ic.ac.uk/ue/ciff/. 4 Our implementation uses the built-in fi nite domain solver of Sicstus Prolog 1, but the modularity of the system would also support the integration of a diff erent solver. occurs. A theory may be regarded a
20、s the (selective) completion of a normal logic program (i.e. of a logic program allowing for negative subgoals in a rule) 2. Any predicate that is neither defi ned nor special is called an abducible. In this paper, the integrity constraints in the set IC (not to be confused with constraint predicate
21、s) are implications of the following form: L1 Lm A1 An Each of the Limust be a literal (with negative literals again being written in implication form); each of the Aimust be an atom. Any variables are implicitly universally quantifi ed with the scope being the entire implication. A query Q is a con
22、junction of literals. Any variables in Q are implicitly existentially quantifi ed. They are also called the free variables. In the context of the CIFF procedure, we are going to refer to a triple hTh,IC,Qi as an input. Semantics. A theory provides defi nitions for certain predicates, while integrity
23、 constraints restrict the range of possible interpretations. A query may be re- garded as an observation against the background of the world knowledge encoded in a given abductive logic program. An answer to such a query would then pro- vide an explanation for this observation: it would specify whic
24、h instances of the abducible predicates have to be assumed to hold for the observation to hold as well. In addition, such an explanation should also validate the integrity con- straints. This is formalised in the following defi nition: Defi nition 1 (Correct answer). A correct answer to a query Q wi
- 配套讲稿:
如PPT文件的首页显示word图标,表示该PPT已包含配套word讲稿。双击word图标可打开word文档。
- 特殊限制:
部分文档作品中含有的国旗、国徽等图片,仅作为作品整体效果示例展示,禁止商用。设计者仅对作品中独创性部分享有著作权。
- 关 键 词:
- The CIFF Proof Procedure for Abductive Logic Programming with Constraints
链接地址:https://www.31doc.com/p-3800783.html