为什么 Mace4 估值在我的 Python 程序中不起作用？

Question

这里是一个非常简单的Mace4的使用例子，直接取自NLTK网站：

from nltk.sem import Expression
from nltk.inference import MaceCommand

read_expr = Expression.fromstring
a = read_expr('(see(mary,john) & -(mary = john))')
mb = MaceCommand(assumptions=[a])
mb.build_model()
print(mb.valuation)

当我打印

mb.valuation

的返回值而不是

mb.build_model()

时，我得到

True

所以模型是正确构建的。但是当我问

print(mb.valuation)

我得到

Traceback (most recent call last):
  File "test2.py", line 8, in <module>
    print(mb.valuation)
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/mace.py", line 51, in valuation
    return mbc.model("valuation")
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/api.py", line 355, in model
    return self._decorate_model(self._model, format)
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/mace.py", line 185, in _decorate_model
    return self._convert2val(valuation_str)
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/mace.py", line 60, in _convert2val
    valuation_standard_format = self._transform_output(valuation_str, "standard")
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/mace.py", line 206, in _transform_output
    return self._call_interpformat(valuation_str, [format])[0]
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/mace.py", line 220, in _call_interpformat
    self._interpformat_bin = self._modelbuilder._find_binary(
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/inference/prover9.py", line 177, in _find_binary
    return nltk.internals.find_binary(
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/internals.py", line 675, in find_binary
    return next(
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/internals.py", line 661, in find_binary_iter
    yield from find_file_iter(
  File "/Users/yannis/miniconda3/lib/python3.8/site-packages/nltk/internals.py", line 620, in find_file_iter
    raise LookupError(f"\n\n{div}\n{msg}\n{div}")
LookupError: 

===========================================================================
NLTK was unable to find the interpformat file!
Use software specific configuration parameters or set the PROVER9 environment variable.

  Searched in:
    - /usr/local/bin/prover9
    - /usr/local/bin/prover9/bin
    - /usr/local/bin
    - /usr/bin
    - /usr/local/prover9
    - /usr/local/share/prover9

  For more information on interpformat, see:
    <https://www.cs.unm.edu/~mccune/prover9/>
===========================================================================

我通过

brew install

安装了Prover9，一切顺利。我做错了什么吗？

Answer 1

报错提示，你的程序找不到prover9。要解决这个问题，您必须找到它的安装位置并将其添加到您的路径中。

通过运行以下命令找到安装路径：

brew --prefix prover9

这应该返回安装 prover9 的路径（类似于 /usr/local/Cellar/prover9/）。

现在，您需要将 PROVER9 环境变量设置为此路径。您可以通过运行以下命令来执行此操作。请记住根据您的 shell 更改文件——

.bashrc

、

.bash_profile

或

.zshrc

。

bash_profile

的示例命令：

echo 'export PROVER9=<PATH_TO_PROVER9>' >> ~/.bash_profile
source ~/.bash_profile

添加此行后，重新启动终端（或运行

source .bashrc

、

source .bash_profile

或

source .zshrc

）以应用更改。

现在，再次运行您的 Python 脚本，错误应该已解决。

---- 替代方法----

如果您仍然遇到问题，您也可以尝试直接在您的 Python 脚本中设置 PROVER9 环境变量：

import os
os.environ['PROVER9'] = '<PATH_TO_PROVER9>'