# Re: a simple question

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>

```

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 GMT

This archive was generated by hypermail 2.2.0+W3C-0.50 : Monday, 7 December 2009 10:53:11 GMT