Re: model theory publication draft

>>  and I think it all goes very well except for rule 1.
>> I currently don't see how to implement that with a back-chaining reasoner.
>> Any hint?
> I guess I don't see what the problem is. Can you elaborate?

of course
we want to see the entailment
  |- rdfs:range rdf:type rdfs:Property.
i.e. out of nothing (besides those rules of course)
now we do this with a back-chaining engine
so we try to satisfy
  rdfs:range rdf:type rdfs:Property.
and to satisfy that, we must satisfy
  :s :p :o.
where :p is unbound (if I may speak that way)
and we just don't find a reasonable way to do that

> Pat
>
> PS. Why do you ever need to backchain? I think you can use the rules as
> though they were a production system: as soon as a LHS matches, fire
> the rule (and check its not duplicating anything) then re-start
> searching from the beginning of the list. If you ever get to the end,
> stop.

agreed, that's certainly a possibility, but we
are trying backchaining, and I believe there
is a possiblilty (maybe something like universal
elimination rule generation???)

PS. we have a similar thing for existential introduction rule
    generation for premis and query statements with unlabeled
    nodes and that works amazingly well

Jos

Received on Thursday, 20 September 2001 18:42:15 UTC