Re: [UCR] RIF needs different reasoning methods

On Mar 6, 2006, at 3:50 AM, Francois Bry wrote:

> Dear All,
>
> At the RIF meeting last week in Mandelieu, I have been asked to
> explain the view that RIF needs different reasoning methods -
> even though it should have a single declarative semantics.

Sorry, I missed the meeting. Are you arguing that RIF documents need to 
be able to *specify* the intended reasoning method for those documents? 
Is this distinct from declaring their intended semantics?

How could one stop there from being different reasoning methods, given 
a declarative semantics (even, say, incomplete or unsound ones; the 
meaning of the document is specified, not, typically, what people 
choose to do with those documents).

> The following is a (sketch of an) application scenario illustrating
> different forms of reasoning with rulesets that, in my opinion, the
> RIF should support.

What is the nature of that support? I mean, pragmatically speaking, 
what needs to be done to enable such support?

[snip]
> A rule like the previous one is similar to a database view (also
> called deduction rule): it gives rise to (deterministically) derive
> new information from information explicitely stated. Simple and
> efficient reasoning techniques (referred to as 'constructive
> reasoning') are sufficient for this, especially no excluded middle or
> refutation are needed.

Isn't resolution a refutation technique? Did you mean something 
stronger?

> Such simple reasoning techniques are
> e.g. forward chaining and backward chaining SLD resolution also called
> (linear resolution without ancestor resolution) as used with
> Datalog. Let refer to such rules as 'deduction rules'.
>
> Dedicated RIF reasoners for deduction rules would be useful for
> generating conclusions - either by forwards or backward chaining -
> from deduction rules.

Aren't you just saying that there is a subset of the RIF for which 
there are known efficient techniques? What more? Is supporting those 
techniques just calling out a named subset?

> 4. Concluding Remarks
> Event hough the declarative semantics of the constructive and of the
> other declarative RIF rules of the application scenario sketched above
> can be formalized in the same manner, e.g. by a Tarsky-style model
> theory, different type of RIF reasoners and/or rule transformers are
> needed.

I guess I'm still confused by the impact of these points on the spec.

> Note that existing OWL reasoners only address 2 above. They can
> perform 1 but at unnecessary costs.

Er...not necessarily. KAON2? Actually, regular tableaux based reasoners 
can do pretty well, depending. (Granted, they do not typically use 
secondary storage, but they can do quite well.)

> They cannot perform 3.
[snip]

Really? I didn't get exactly what 3 was. Is this anything more than 
efficient view/truth maintenance? (If so, there is some work in this 
direction.)

I don't understand the emphasis on implementation details.

Cheers,
Bijan.

Received on Monday, 6 March 2006 10:19:09 UTC