AI*IA 2003: Advances in Artificial Intelligence 8th Congress of
This book constitutes the refereed proceedings of the 8th Congress of the Italian Association for Artificial Intelligence, AI*IA 2003, held in Pisa, Italy in September 2003. The 44 revised full papers presented were carefully reviewed and selected from 91
- PDF / 7,265,587 Bytes
- 567 Pages / 430 x 660 pts Page_size
- 75 Downloads / 205 Views
Abstract. Efficiency of the first-order logic proof procedure is a major issue when deduction systems are to be used in real environments, both on their own and as a component of larger systems (e.g., learning systems). Hence, the need of techniques that can perform such a process with reduced time/space requirements (specifically when performing resolution). This paper proposes a new algorithm that is able to return the whole set of solutions to θ-subsumption problems by compactly representing substitutions. It could be exploited when techniques available in the literature are not suitable. Experimental results on its performance are encouraging.
1
Introduction
The classical Logic Programming [8] provability relation, logic implication, has been shown to be undecidable [12], which is too strict a bias to be accepted. Hence, a weaker but decidable generality relation, called θ-subsumption, is often used in practice. Given C and D clauses, C θ-subsumes D (often written C ≤ D) iff there is a substitution θ such that Cθ ⊆ D. A substitution is a mapping from variables to terms, often denoted by θ = {X1 → t1 , . . . , Xn → tn }, whose application to a clause C, denoted by Cθ, rewrites all the occurrences of variables Xi (i = 1 . . . n) in C by the corresponding term ti . Thus, since program execution corresponds to proving a theorem, efficiency of the generality relation used is a key issue that deserves great attention. In the following, we will assume that C and D are Horn clauses having the same predicate in their head, and that the aim is checking whether C θsubsumes D. Note that D can always be considered ground (i.e., variable-free) without loss of generality. Indeed, in case it is not, each of its variables can be replaced by a new constant not appearing in C nor in D (skolemization), and it can be proven that C θ-subsumes D iff C θ-subsumes the skolemization of D. | · | will denote, as usual, the cardinality of a set (in particular, when applied to a clause, it will refer to the number of literals composing it). Since testing if C θ-subsumes D can be cast as a refutation of {C} ∪ ¬D, a basic algorithm can be obtained in Prolog by skolemizing D, then asserting all the literals in the body of D an the clause C, and finally querying the head of D. The outcome is computed by Prolog through SLD resolution [10], which can be very inefficient under some conditions, as for C and D in the following example. A. Cappelli and F. Turini (Eds.): AI*IA 2003, LNAI 2829, pp. 1–13, 2003. c Springer-Verlag Berlin Heidelberg 2003
2
Stefano Ferilli et al.
Example 1. C = h(X1 ) :- p(X1 ,X2 ),p(X2,X3 ),...,p(Xn−1,Xn ),q(Xn). D = h(c1 ) :- p(c1 ,c1 ), p(c1 ,c2 ), ..., p(c1 ,cn ), p(c2 ,c1 ), p(c2 ,c2 ), ..., p(c2 ,cn ), ..., p(cn ,c1 ), p(cn ,c2 ), ..., p(cn ,cn ). In the following, the next section presents past work in this field; Section 3 presents the new θ-subsumption algorithm, and Section 4 shows experimental results concerning its performance. Lastly, Section 5 concludes the paper.
2
Related Work
The great importance of finding
Data Loading...
