Re: Rules WG -- draft charter

From: "Jos De_Roo" <jos.deroo@agfa.com>
Subject: Re: Rules WG -- draft charter
Date: Tue, 11 Nov 2003 02:48:47 +0100

> 
> 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 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 or to make the impossible possible so I'm not very optimistic that
> > 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.

I think that proofs for Horn clause knowledge bases can be arbitrarily long
in the size of the knowledge base. (Consider an encoding of the word
problem in Horn clauses.)  Although it may be easy to check each step of
the proof, it would be decidedly not easy to check the entire proof.
Builtins can't really help here - any builtin that does not perform
drastic reduction in the size of the proof will not be effective but any
builtin that does adequate size reduction will make checking each step
difficult.

> > 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.

This really isn't going to help in the worst case.  You just can't make
all the hard problems disappear in this way.

[...]

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

Peter F. Patel-Schneider
Bell Labs Research

Received on Monday, 10 November 2003 21:09:42 UTC