Prover9導入方法

入門自然言語処理にて、nltkで使用する定理証明器であるProver9のインストール方法でちょっと迷ったので、メモしておきます。

まずはDL

$ wget http://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz

そして解凍

$ tar xvzf LADR-2009-11A.tar.gz 

名前をちょっと変えてあげて

$ mv LADR-2009-11A prover9

$ cd prover9/

インストール

$ make all

なにやらこれを入力しろと言われるのでごにょごにょ

$ make test1

$ make test2

$ make test3

最後にシンボリックリンクを張って完了

$ sudo ln -s /home/vagrant/prover9/bin/prover9 /usr/local/bin/

無事にnltkで使用することが出来ました。

sample.py

# -*- coding: utf-8 -*-
#from __future__ import division
import nltk,re

lp = nltk.LogicParser()
SnF = lp.parse('SnF')
NotFnS = lp.parse('-FnS')
R = lp.parse('SnF -> -FnS')
prover=nltk.Prover9()
print prover.prove(NotFnS,[SnF,R])