Question: Is it possible to check if x*y*z is zero assuming x*z is zero?

SymPy's Assumption System

SymPy can handle the following query to its assumption system:

>>> from sympy import Q, ask
>>> from sympy.abc import x, y, z
>>> ask(Q.zero(x*y*z), Q.zero(x*z) & Q.real(y))
True
>>> ask(Q.zero(x*y*z), (Q.zero(x) | Q.zero(z)) & Q.real(y))
True
>>> ask(Q.zero(x*y) | Q.zero(y*z), Q.zero(x*z) & Q.real(y))
True

Mathematica's Assumption System

Mathematica can handle an equivalent query:

In[21]:= Assuming[{x*z == 0}, Refine[x*y*z == 0]]
Out[21]= True

However, it can't handle a similar type of query:

In[25]:= Assuming[{x == 0 || z == 0}, Simplify[x*y*z == 0]]
Out[25]= x y z == 0

In[28]:= Assuming[{x*y == 0}, Refine[x*z == 0 || z*y == 0]]
Out[28]= x z == 0 || y z == 0  

Maple's Assumption System

It seems that Maple can't handle this type of query at all:

> with(RealDomain);
> is(x*y*z = 0) assuming (x*z = 0, y::real);
FAIL   

However, Maple can handle simpler assumptions like x = 0:

> is(x*y*z = 0) assuming (x = 0, y::real, z::real);
true

Is there some way to use Maple's assumption system to reason about assumptions like x*y=0? I believe that's not possible. If Maple can infer either x=0 or y=0 from x*z=0, its assumption system doesn't seem to be capable of dealing with this sort of assumption.

Based on a paper by Weibel and Gonnet (1993), it doesn't seem like Maple can reason about assumptions that are disjunctions of properties for more than one variable, such as "property p holds for x OR property p holds for y."

SymPy can handle these sorts of queries because it uses a SAT solver as part of its assumption system. However, there is no mention of a SAT solver—or any method of checking multiple possibilities—in the referenced paper or related papers on Maple's assumption system.

Am I correct that Maple's assumption system is not capable of handling this sort of query?

Reference

Weibel, T., Gonnet, G.H. (1993). An assume facility for CAS, with a sample implementation for Maple. In: Fitch, J. (ed) Design and Implementation of Symbolic Computation Systems. DISCO 1992. Lecture Notes in Computer Science, vol 721. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57272-4_27

By the way, is there some way to use markdown for these questions? I made the above post by asking chatgpt to convert markdown into html. 

Please Wait...