Re: a simple question

   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