Re: Problem with damlsParameter

On Tuesday, April 22, 2003, at 09:02 AM, Drew McDermott wrote:

>    [Bijan Parsia]
>       [Daniel Elenius]
>> It doesn't make sense to me, and I can see why it doesn't make sense to
>> the JTP reasoner, it being very logical after all :)
>
>    No, it just means that you don't have the right axioms.
>
> There may be a technical limitation of JTP that prevents it from
> making assertions about predicates.

Oops, I really should have said "don't have the right axioms or 
reasoner".

However, I do believe Pat Hayes worked pretty hard on the RDFS semantics 
to make it workable with first order reasoners (for example).

You could start from the LBase axiomization of RDFS:
	http://www.w3.org/TR/rdf-mt/#Lbase

(triple version: http://www.w3.org/TR/rdf-mt/#rdfs_interp)

Hmm. I thought that they were going to go the DAML+OIL axiom route and 
represent triples as triples. I'm not quite what's up...

...aha, the LBase doc explains further:
	http://www.w3.org/2002/06/lbase/20030116Snapshot.html
Key bit being:

"""The explicit extension mapping is a technical device to allow 
relations to be applied to other relations without going outside 
first-order expressivity. We note that while this allows the same name 
to be used in both an individual and a relation position, and in a sense 
gives relations (and hence functions) a 'first-class' status, it does 
not incorporate any comprehension principles or make any logical 
assumptions about what relations are in the domain. Notice that no 
special semantic conditions were invoked to treat variables in relation 
position differently from other variables. In particular, the language 
makes no comprehension assumptions whatever. The resulting language is 
first-order in all the usual senses: it is compact and satisfies the 
downward Skolem-Lowenheim property, for example, and the usual 
machine-oriented inference processes still apply, in particular the 
unification algorithm. (One can obtain a translation into a more 
conventional syntax by re-writing every atomic sentence using a rule of 
the form R(t1,...,tn) => Holds(R, t1,...,tn), where 'Holds' is a 'dummy' 
relation indicating that the relation R is true of the remaining 
arguments. The presentation given here eliminates the need for this 
artificial translation, but its existence establishes the first-order 
properties of the language. To translate a conventional first-order 
syntax into the Lbase form, simply qualify all quantifiers to range only 
over non-Relations. The issue is further discussed in (Hayes & Menzel 
ref). )"""

I suspect that you might have to use the Holds(_,_,_) translation to get 
it to work with many TPs.

>  However, if it's based on Kif
> there shouldn't be any such limitation, because Kif allows such
> assertions.

At the moment, alas, there's no LBase translation for OWL (that I see). 
So one might have to start with the (flawed) DAML+OIL axiomatic 
semantics (which is in KIF) and update.

Cheers,
Bijan Parsia.