# Re: a simple question

From: pat hayes <phayes@ihmc.us>
Date: Tue, 2 Dec 2003 19:21:15 -0600
Message-Id: <p06001f18bbf2e73748bb@[10.1.31.1]>
To: Drew McDermott <drew.mcdermott@yale.edu>

```
>    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

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