这里是一个非常简单的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,一切顺利。我做错了什么吗?
报错提示,你的程序找不到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>'