On Thu, Mar 8, 2018 at 6:24 PM, Tom Lane <t...@sss.pgh.pa.us> wrote: > * R1: A refutes B if truth of A implies falsity of B. > * R2: A refutes B if truth of A implies non-truth of B. > * R3: A refutes B if non-falsity of A implies non-truth of B. > * R4: A refutes B if non-falsity of A implies falsity of B.
The use of the terms "refutes", "non-truth", and "non-falsity" drive me a little batty; they've all got an internal negation built into them, and that's confusing. It seems very tempting to propose getting rid of predicate_refuted_by altogether and to simply have one function: if we know that everything in clause_list is { true | false } [ or null ], does that imply that everything in predicate_list must be { true | false } [ or null ]? Internally, we could represent what we know about various clauses by some combination of CLAUSE_MIGHT_BE_TRUE = 0x01, CLAUSE_MIGHT_BE_FALSE = 0x02, CLAUSE_MIGHT_BE_NULL = 0x04. I have a feeling this might work out to be a lot easier to understand than what we've got now, because saying that "A weakly refutes B" is a heck of a lot less clear, at least in my book, than saying "If A is true or null, B must also be true or null." I realize this is all a little to one side of what you're talking about here, but the fact that even you got confused about whether the existing logic was correct, and that you found that there were multiple possible definitions of what "correct" means, seems like pretty good evidence that this is not as clear as it could be. -- Robert Haas EnterpriseDB: http://www.enterprisedb.com The Enterprise PostgreSQL Company