其实，呈现这个题目很简单。会有三种可能：

1、没有安装Prover9。你可以按照这个链接进行：http://www.cs.unm.edu/~mccune/mace4/download/LADR1007B-win.zip（合适Windows体系），若是你的操纵体系是此外，那么也有相对应的版本，可以去官网进行。

那么第2种可能，就是设置不当，还是会造成无法找到Prover9这个错误。

按照Python的提示，“PROVER9HOME environment variable”我们须要本身设置一个体系变量来使法度持续进行，当然也可以应用Python自带的设置函数。这里只介绍体系变量的办法。

按照它的提示，我们须要添加如许一个变量，PROVER9HOME。从源代码傍边也可以看出这一点。

if  path is  None:

        searchpath = prover9_search

        if PROVER9HOME in os.environ:

            searchpath.（0， os.environ[PROVER9HOME]）

在这里我说一下，我的Prover9的文件路径：D:\SpecialSoftware\prover9\bin （要重视，变量的值要写到bin，网上有些解决规划说只写到prover9为止，这是模糊的，不正确的，不然依然会造成无法找到的成果）

3、若是景象变量设置完了，仍然还是无法找到，那么你就要测验测验封闭Python编辑窗口，从头打开，再试一下。这个时辰应当没有题目了。

若是以上规划都不可，你就要检测你的景象变量的路径是不是设置的不合错误。建议你在Python窗口中输入号令进行搜检：

>>> import os

>>> os.environ[PROVER9HOME]

D:\\SpecialSoftware\\prover9\\bin