From: Drew McDermott <drew.mcdermott@yale.edu>

Date: Tue, 2 Dec 2003 13:57:33 -0500 (EST)

Message-Id: <200312021857.hB2IvX004336@pantheon-po03.its.yale.edu>

To: public-sws-ig@w3.org, www-rdf-rules@w3.org

Date: Tue, 2 Dec 2003 13:57:33 -0500 (EST)

Message-Id: <200312021857.hB2IvX004336@pantheon-po03.its.yale.edu>

To: public-sws-ig@w3.org, www-rdf-rules@w3.org

Suppose we have a simple service having as input the current location of = a user and as output the nearest airport. I suppose that the web service should describe what "nearest" means. A = way to describe this, I think, is by using rules.=20 Probably the definition of "nearest" could be: nearest(current_location, X) :- airport(X), airport(Y), X =\= Y, (location(X) - current_location) <= (location(Y) - current_location). Could anybody explain me how I can use OWL Rule Language [1] in = specifying such a rule, taking=20 into account that in OWL Rule Language only variables that occur in the = antecedent of a rule may occur in the consequent. The rule you gave doesn't say what you want. It says that X is the nearest if there exists a Y (not = X) such that X is closer than Y. In fact, the existence of such a Y is neither a necessary nor a sufficient reason for Y to be nearest. The correct way to say it is nearest(current_location, X) :- airport(X), forall (Y) (airport(Y) -> (location(X) - current_location) <= (location(Y) - current_location)) (The inequality condition is unnecessary, although harmless). To eliminate the explicit quantifier, there are two approaches one can take. One is to skolemize, replacing Y by a term sk_nst(X): nearest(current_location, X) :- airport(X), (airport(sk_nst(X)) -> (location(X) - current_location) <= (location(sk_nst(X)) - current_location)) A theorem prover might use this as follows: To prove that JFK is the nearest airport, verify that JFK is an airport, then assume that sk_nst(JFK) is an arbitrary airport, and prove that (location(sk_nst(JFK)) - current_location) is > (location(JFK) - current_location) You probably won't be able to prove this unless you have a list of all the airports, so that you can infer sk_nst(JFK) = BDL V sk_nst(JFK) = LAX V sk_nst(JFK) = GTW V ... Then case analysis and equality substitution would finish the proof off. The alternative is to use negation-as-failure, writing the axiom nearest(current_location, X) :- airport(X), (\+ (airport(Y), (location(X) - current_location) > (location(Y) - current_location))) where \+ is the usual Prolog symbol for negation-as-failure. This version says, in essence, if I can't think of an airport Y that is closer than X to my current location, then X is the nearest airport. The NAF approach is likely to be much more efficient, much easier to implement, and much more likely to yield a useful conclusion than the heavy-duty theorem prover. I hope the people who deprecate it realize that the heavy-duty theorem prover is the only alternative. -- -- Drew McDermott Yale University CS Dept.Received on Tuesday, 2 December 2003 13:57:34 UTC

*
This archive was generated by hypermail 2.3.1
: Wednesday, 2 March 2016 11:10:15 UTC
*