可以检查x*y*z是否为零，假设x*z在枫树中为零？

Question

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

，但是，似乎枫树根本无法处理这种类型的查询。

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

themaple可以处理更容易的假设。

x = 0

有一些方法可以使用枫树的假设系统来推理诸如

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

之类的假设？我认为这是不可能的，因为如果枫树能够从

x*y=0

推断

x=0

或

y=0

x*z=0

，它的假设系统就无法处理这种假设。
Weibel and Gonnet（1993）的论文基于一份论文，似乎枫树似乎无法理解一个假设，这些假设是多个变量的属性分析的假设，例如“ x或property P符合Y”的属性P，y” .

Sympy可以处理这些查询，因为它使用SAT求解器作为其假设系统的一部分。但是，在该论文或相关论文中，没有提及SAT求解器或任何形式检查多种可能性的方法。 我纠正了枫树的假设系统无法处理这种查询吗？ Reference Weibel，T.，Gonnet，G.H。 （1993）。 CAS的假设设施，并为枫木实现样本。在：Fitch，J。（ED）

设计和符号计算系统的实现。迪斯科1992年。计算机科学的讲义，第721卷。施普林格，柏林，海德堡。 

https：//doi.org/10.1007/3-540-57272-4_27

还有其他一些进行此类查询的机制，

is(x*y*z = 0) assuming Or(x=0,z=0);

       true

simplify(x*y*z, {x*z=0});

         0

is(simplify(x*y*z=0, {x*z=0}));

       true

algsubs(x*z=0, x*y*z);

         0

is(algsubs(x*z=0, x*y*z=0))

       true