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.

All true. It is also likely to be wrong, 
unfortunately. The fact that you can't think of a 
closer airport doesn't usually qualify as a good 
reason to conclude that there isn't one, unless 
you also know for sure that you know all the 
airport locations, so that if you don't know it, 
then its not there. Like, for example, if you 
have a  list of all the airports. If you make 
this explicit, as you should, then you are back 
doing 'heavy-duty' reasoning.

BTW, calling it 'heavy-duty' is misleading. In 
the first case you have made all the equality 
reasoning explicit. In a prolog-style 
implementation this is all buried in the 
backtracking done by the interpreter: but it 
still needs to be done. The same actual 
*reasoning* is involved in both cases.

>  I hope the people who deprecate it realize
>that the heavy-duty theorem prover is the only alternative.

Its not a matter of alternatives. If you want to 
draw checkable valid conclusions, then you need 
to do this kind of reasoning.  If you want to 
make random guesses and hope for the best then 
you can of course work faster, but don't expect 
others to believe in your conclusions. 
Negation-as-failure is NOT a good general 
reasoning strategy: 99.99% of the time it will 
immediately produce childishly ludicrous 
conclusions: I don't know anyone called Jose, so 
there isn't anyone called Jose; I never heard of 
SARS, so there is no disease called SARS, so 
nobody can possibly have died from SARS; and so 
on. It is of utility only in those very special 
circumstances when you have some reason to be 
confident that you are dealing with a 'complete' 
source of information about some aspect of some 
topic (like having a list of all the airports. 
Even then you had better be careful: is it really 
ALL the airports or only those with an 
international airport code? Does it include civil 
airports and military airfields?). When you do, 
of course, then it is indeed very handy.  The 
industrial uses of Prolog-style rules all are 
designed within controlled environments, 
typically using databases, where such special 
conditions can be assumed. But on the web, we 
can't assume that we are living in such a 
controlled environment. We need to make those 
critical assumptions explicit somehow if we are 
going to make rules that can survive in the real 
world.

Pat Hayes

>--
>                                              -- Drew McDermott
>                                                 Yale University CS Dept.


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes@ihmc.us       http://www.ihmc.us/users/phayes

Received on Tuesday, 2 December 2003 20:23:10 UTC