Hello, On Tue, Feb 10, 2009 at 09:41:46PM +0100, Dimitri Fontaine wrote: > 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...
formal theorem proving and mechanized mathematics happen to be one of my research topics in the last few years; so I think that my experience could be helpful with such problems. (Actually instead of Coq I use HOL Light, whereas other people in my research group work with Coq; but both of them are for the same purpose) Perhaps a way to begin would be to start writing a formalization of the above rules, in order to assess the problem quickly, and then to get back to pg-hackers soon. Any comments/warnings/suggestions ? Thank you, Dr. Gianni Ciolli - 2ndQuadrant Italia PostgreSQL Training, Services and Support gianni.cio...@2ndquadrant.it | www.2ndquadrant.it -- Sent via pgsql-hackers mailing list (pgsql-hackers@postgresql.org) To make changes to your subscription: http://www.postgresql.org/mailpref/pgsql-hackers