Re: Rules WG -- draft charter

PFPS:
> From: "Jos De_Roo" <jos.deroo@agfa.com>
> Subject: Re: Rules WG -- draft charter
> Date: Tue, 11 Nov 2003 01:26:26 +0100
>
>> PeterPS:
>> [...]
>>> It is generally the case that proof checking is no harder than proving,
>>> although I don't remember a proof to this effect.  :-)
>>
>> :-)
>>
>>> It is certainly the case that proof checking is usually easier than
>>> proving, and mostly proof checking is very much easier than proving,
but
>>
>> That's what I also thought...
>>
>>> this is certainly not always the case.
>>
>> It is an engineering challenge to avoid those cases :-)
>> and here I believe so called "builtins" could help
>> (at least that's our experience with such cases
>> as http://www.agfa.com/w3c/2002/10/medicad/op/index.html
>> esp http://www.agfa.com/w3c/2002/10/medicad/op/lldmE.n3
>> or http://www.agfa.com/w3c/2002/10/medicad/op/lldmE2.n3)
>
> I don't think that it is ``engineering'' to either make the awkward
> disappear to make the impossible possible so I'm not very optimistic that
           ^or ??
> engineering is going to help here.

That's an opinion... plus
why would one try to make the awkard disappear or the impossible possible?
That example was just intended to illustrate derivations and ordinary
computations, not more, not less and it works in a very simple way
and I believe the proof is really easy to check (due to the limitation
of using just Horn clauses and primitive mathematical builtins).
There are of course many other examples.

> Perhaps you mean that it is the task of the yet-to-be-chartered working
> group to only use logics where proof checking is easier than proving.

Well, I was just thinking about builtins to avoid exponentially lenghty
proofs but indeed, those builtins have to be understood by all parties.

> Maybe, but I would think that some better guidance would go a long way in
> preventing potential delay and heartache.

Yes, we need guidance...


>> Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/
>
> Peter F. Patel-Schneider
> Bell Labs Research

--
Jos De Roo, AGFA http://www.agfa.com/w3c/jdroo/

Received on Monday, 10 November 2003 20:49:03 UTC