在Maple中基于x*z=0的假设，能否判定x*y*z是否为零？

SymPy的假设系统表现 #

SymPy的假设系统可处理以下涉及乘积零、析取条件的查询：

>>> 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的表现 #

Mathematica可处理部分等效查询：

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

Out[21]= True

但它无法处理部分同类型的查询：

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的表现 #

然而，Maple似乎完全无法处理这类涉及乘积零的复合假设查询：

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

Maple仅能处理诸如x = 0这类单一变量的简单假设：

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

问题与分析 #

是否存在方法让Maple的假设系统处理x*y=0这类复合假设？我认为这不可行，因为若Maple能从x*z=0推导出x=0或z=0，反而说明其假设系统无法处理此类析取性的复合假设。

根据Weibel与Gonnet在1993年发表的论文，Maple似乎无法对涉及多个变量属性析取的假设进行推理，例如“属性p适用于x或属性p适用于y”这类场景。

SymPy可处理这类查询是因为其假设系统集成了SAT求解器，但该论文及相关文献中均未提及Maple使用SAT求解器或任何多可能性检查方法。

我的判断是否正确——Maple的假设系统确实无法处理这类查询？

参考文献 #

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.

内容的提问来源于stack exchange，提问作者Tilo RC