【问题和解决】NLTK was unable to find the prover9 file!

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

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.insert(0, os.environ['PROVER9HOME'])

在这里我说一下，我的Prover9的文件路径：D:\SpecialSoftware\prover9\bin (要注意，变量的值要写到bin，网上有些解决方案说只写到prover9为止，这是含糊的，不正确的，否则依然会造成无法找到的结果)

3、如果环境变量设置完了，仍然还是无法找到，那么你就要尝试关闭Python编辑窗口，重新打开，再试一下。这个时候应该没有问题了。

如果以上方案都不行，你就要检测你的环境变量的路径是不是设置的不对。建议你在Python窗口中输入命令进行检查：

>>> import os
>>> os.environ['PROVER9HOME']
'D:\\SpecialSoftware\\prover9\\bin'