In the introductory natural language processing, I was a little confused about how to install Prover9, which is the theorem proving device used in nltk, so make a note of it.
First of all, DL
$ wget http://www.cs.unm.edu/~mccune/mace4/download/LADR-2009-11A.tar.gz
And defrost
$ tar xvzf LADR-2009-11A.tar.gz
Change the name a little
$ mv LADR-2009-11A prover9
$ cd prover9/
Installation
$ make all
I'm asked to enter this, so I'm gonna go
$ make test1
$ make test2
$ make test3
Finally, make a symbolic link and complete
$ sudo ln -s /home/vagrant/prover9/bin/prover9 /usr/local/bin/
I was able to use it with nltk safely.
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])
Recommended Posts