wolfram-mathematica – 性能问题：在Mathematica中通过几个假设来解决不等式问题

我需要证明一个不等式(或找到一个反例)给出几个假设(也就是不等式).不幸的是,要证明的不平等是一个相当漫长而复杂的表达.大约有15个变量,FullSimplify的输出填充了几个A4页面.对于变量较少的示例,如果不等式为真,FindInstance有助于找到反例或给出{}的结果.我也尝试过以这种方式使用Reduce：

Reduce[
   Implies[
      assumtion1 && assumtion2,
      inequality
   ],
   Reals
]

对于简单的例子,如果不等式成立,则输出“True”.但在我的情况下,经过几个小时的运行时间,Mathematica需要5-6 GB的RAM(和交换),所以我不得不中止这个过程.

我可以用Mathematica做些什么来提高性能吗？

你会在Mma CAD算法 here上找到一篇非常好的论文

Mma使用的圆柱代数分解(CAD)在变量数量上以双指数行为进行缩放.

较新的方法在量化器交替的数量中是双指数的.

我认为你只使用Mma内置引擎没有运气,但你可以根据问题的对称性(如果有的话)推出自己的引擎