Re: [UCR] RIF needs different reasoning methods

On Mar 10, 2006, at 8:50 AM, Gerd Wagner wrote:

> Bijan Parsia wrote:
>> What I don't see is the reason for specifying particular proof
>> procedures *instead of* expressive subsets.
>> If two reasoners perform acceptibly and give the same answers...
>> what *more* do you need?
>
> Ian Horrocks wrote:
>> Given that a particular prover has an adequate response time and
>> provides correct answers (as defined by the semantics), then why
>> would I care what procedure it uses in order to do its work?
>
> Bijan and Ian, you didn't get the point:

Hence the continued querying. I am trying to tease out what was 
intended. Frankly, it just hasn't been clear.

> rule processing is
> not just reasoning (the world is not that simple), and rule
> interchange is not just an exchange of implication formulas
> between "reasoners" (it's an old misconception of AI that
> intelligent life is all about reasoning).

Red herring. No one argued that. We've argued that *if* all you care 
about is the answers to queries and *if* the only other consideration 
is efficiency *then* talking about different proof strategies doesn't 
seem to help.

Yet both the antecedents are, afaict, explicitly articulated in 
Francois' posts and examples. When I try to probe for the falsity of 
one, I am rebuffed. Hence my confusion.

> Most rule processing
> in real life is not involving (much) reasoning, given the fact
> that production rules and ECA/reaction rules are more important

Yet the only articulated differences *in this exchange* 1) typological 
(i.e., a brute assertion of difference), 2) efficiency, and 3) the form 
of the query (as Ed pointed out). What is being asked is what are the 
differences that make a difference based on the *proof* theory. 
Personally, I would prefer to *abstract out* the mention of proof 
theory into the features of the proof theory that make the difference. 
For example, if you require the results to come in a certain order 
corresponding to the behavior of a (very specific proof theory) then 
let's require *that ordering*. How an implementation gets that ordering 
is up to it.

Similarly, if reaction rules are *solely* being used to supply certain 
answers, then let's not overconstrain the situation. Specify what the 
answers are and leave it to implementations to supply those answers as 
they see fit. If my implementation doesn't meet your efficiently needs 
(*regardless of the proof procedure I implement*) then don't use me. 
(Crappy implementations of theoretically superior algorithms can suck 
hard.)

> in IT systems than any form of derivation/deduction rules.
> Changing the state of a system and detecting complex events is
> not the domain of FOL.

Yes, but Francois has not mentioned these features in a distinguishable 
way. Perhaps they *become* distinguishable in the presence of more 
features (e.g., in the query language), but then let's look toward 
*that*.

> Francois just tried to point out that there are these different
> types of rules, and they cannot all be processed in the same
> manner (with "reasoners"). And even for "reasoning rules",
> there is a computational logic distinction between
>
> - rules for making definitions: constructive derivation rules,
>   called "views" in SQL
> - rules for constraining the possible states (and execution
>   histories) of a system: integrity rules/constraints
> - rules for expressing defaults and heuristics: nonmonotonic
>   derivation rules

But please don't equivocate. AFAICT, all of these have expressivity 
differences. Which no one has argued against marking.

> And none of these computational logic distinctions are
> reflected in standard FOL (and neither are they in OWL/SWRL):
> you can't simply combine them and submit their merge to
> a "reasoner"!

Well, I didn't propose that. Who has? Does no one grasp the 
*conditional* nature of Ian's and my queries?

> Does the RIF (or the W3C) intend to ignore these distinctions?

I don't think so, but they do need to me made clearer and more 
substantive than they have be. If you read over my messages, I hope you 
see that I've tried to propose example distinctions that made sense to 
me, only to be told that I got it wrong, that the semantics really 
*are* the same, but the proof theories *need* to be different and 
specified. Why? for efficiency. But, uh, if I can make my tableau 
system run for those queries as efficiently as your Rete engine for 
those rules...*why do you care about the proof procedure*? I'm not 
arguing that you *shouldn't* care, I really want to know what are the 
specific grounds for caring and what the best way to mark the 
distinctions are. I can imagine many, but it's been frustratingly hard 
to get an answer. The accusations aren't helping either.

(For example, I clearly said that if there is a difference that 
mattered in the answer given to the same query, then, *for me*, counted 
as a difference in the semantics of the rules. Of course, I want to 
mark that. But I want to mark that in the least constraining way 
possible. Which for me, precludes saying "proof theory". Operational 
semantics, sure. But Proof Theory suggests something way more specific 
and much closer to implementation than I like. If details of the 
operational (formal) semantics matter, but two systems are 
observationally equivalent from the formal operational semantics 
pov...why should I *care* how the systems achieve that? Well one reason 
might be efficiency. But *efficiency is orthoganal to proof technique*, 
in some sense. That is, if the semantics are the same (up to my 
desire), and the system is efficient enough, what's left for me to care 
about?)

Cheers,
Bijan.

Received on Friday, 10 March 2006 16:58:29 UTC