Hi,
Le 10 févr. 09 à 21:10, Tom Lane a écrit :
> I wrote (in response to Kevin Grittner's recent issues):
>> Reflecting on this further, I suspect there are also some bugs in the
>> planner's rules about when semi/antijoins can commute with other
>> joins;
>
> After doing some math I've concluded this is in fact the case. Anyone
> want to check my work?
I don't know how easy it would be to do, but maybe the Coq formal
proof management system could help us here:
http://coq.inria.fr/
The harder part in using coq might well be to specify the problem the
way you just did, so...
HTH,
--
dim