Menu
▾
▴
#379 Extend reasoners on set extensions to partitions
Several reasoners handle set extension literals, such as “remove membership” and “proof by cases” (since FR [#372] was implemented). However, if a predicate uses a set which is a partition instead, the reasoners are not applicable anymore (e.g., if we can apply a reasoner to x ∈ {a, b}, we can't apply it to x ∈ S, knowing that partition(S, {a}, {b})).
It would be useful to extend these reasoners to handle this case too.
Related
