Re: Rules WG -- draft charter

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
engineering is going to help here.  

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.
Maybe, but I would think that some better guidance would go a long way in
preventing potential delay and heartache.

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

Peter F. Patel-Schneider
Bell Labs Research

Received on Monday, 10 November 2003 19:50:28 UTC