AngouriMath

Navigation

← Back to list of members

Implication​(AngouriMath.​Entity,​AngouriMath.​Entity,​AngouriMath.​Entity.​Variable)

 Method (no overloads)

Summary

a implies b holds where a fails or where b holds, and the first
half of that is a set-builder rather than a complement.

Remarks

This used to read expr.Codomain \ Solve(a) \/ Solve(b), taking the
complement inside the statement node's codomain. That is
Boolean for every Impliesf, so
(x = 1) implies (x = 2) was answered { 2 } \/ BB — a solution set for
a numeric question containing True and False. That is exactly the
confusion between a codomain and a set that
#996 is about,
and a TODO here asked for a universal set to subtract from instead.
Neither is needed. "The values of x where a does not hold" is
{ x : not a }, which names no universe at all — a set-builder is already this
library's unconstrained set, and a complement written that way is right whatever
x ranges over. Which is #996's answer: what the solver wanted was the
difference, and the difference is expressible without the universe.
It does not make the implication solver complete. Solve(b, x) is still
Empty where b does not mention x, so
A implies True comes back as { A : not A } and not as BB — as it
did before, where the answer was BB \ { True }. What this stops is answering
with a set the question was never asked over.

























Angouri © 2019-2023 · Project's repo · Site's repo · Octicons · Transparency · 4378 pages online