Python程序中Mace4 valuation无法正常工作的问题求助

测试代码（来自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.build_model()返回True，说明模型已成功构建，但执行print(mb.valuation)时触发报错，提示NLTK找不到interpformat文件。

已尝试的操作 #

• 通过brew install prover9完成Prover9安装，过程无异常
• 执行brew --prefix prover9得到路径/usr/local/opt/prover9
• 在.bash_profile中配置PROVER9环境变量
• 在Python脚本中通过os.environ['PROVER9']指定路径
• 手动将路径添加到NLTK的prover9.py脚本中

报错信息 #

初始报错 #

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无法找到interpformat文件！
请使用软件特定配置参数或设置PROVER9环境变量。

  搜索路径：
    - /usr/local/bin/prover9
    - /usr/local/bin/prover9/bin
    - /usr/local/bin
    - /usr/bin
    - /usr/local/prover9
    - /usr/local/share/prover9

  关于interpformat的更多信息，请参考相关官方文档
===========================================================================

添加路径后的报错 #

Traceback (most recent call last):
  File "test-mace.py", line 10, 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 178, 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无法找到interpformat文件！
请使用软件特定配置参数或设置PROVER9环境变量。

  搜索路径：
    - /usr/local/bin/prover9
    - /usr/local/bin/prover9/bin
    - /usr/local/bin
    - /usr/bin
    - /usr/local/prover9
    - /usr/local/share/prover9
    - /usr/local/opt/prover9

  关于interpformat的更多信息，请参考相关官方文档
===========================================================================

解决方法 #

1. 检查Prover9安装目录是否包含interpformat
   执行以下命令查看brew安装的Prover9目录下是否存在该工具：

   ls /usr/local/opt/prover9/bin
   

   如果目录中没有interpformat，说明brew提供的Prover9包不包含该组件，需要手动下载完整的Prover9安装包。

2. 手动指定完整路径
   若确认interpformat存在于/usr/local/opt/prover9/bin目录，可在代码中直接指定该路径：

   import os
   from nltk.sem import Expression
   from nltk.inference import MaceCommand
   
   os.environ['PROVER9'] = '/usr/local/opt/prover9/bin'
   
   read_expr = Expression.fromstring
   a = read_expr('(see(mary,john) & -(mary = john))')
   mb = MaceCommand(assumptions=[a])
   mb.build_model()
   print(mb.valuation)
   

3. 重新安装完整Prover9包
   若brew安装的版本缺失组件，可下载完整的Prover9压缩包，解压后将其bin目录设置为PROVER9环境变量，确保interpformat在该目录下。

内容的提问来源于stack exchange，提问作者yannis