Basic FOL question using ResolutionProver

[Mark Woodward]

I am trying to make a basic statement about the symmetry of parent and child.

'all x.(all y.(parentof(y, x) <-> childof(x, y)))'

But with this statement, the ResolutionProver allows me to prove anything as true. e.g. 'foo(Bar)'.

Please see my question on SO: https://stackoverflow.com/questions/43507770/basic-first-order-logic-inference-fails-for-symmetric-binary-predicate

Thank you,

-Mark

[Mark Woodward]

Dmitri Chubnav replied to the SO posted, and does seem that there is a bug in ResolutionProver. 

I am thinking of diving in and fixing the bug, but I wanted to check if anyone thought that there is a good reason not to do this? i.e. is nltk on its way out and I should be using something else?

I was also going to extend ResolutionProver to have a depth limited search feature. e.g. find a contradiction involving 10 or fewer resolution steps, if one exists. Prover9 seems to work well, but it does not appear to have the depth limited feature that I am looking for.

I am generating FOL "worlds", and I need a prover in order to generate a consistent world; i.e. check if the newest sentence would result in a contradiction with the existing sentences (if prove(-new_sentence) then it would result in a contradiction).

Let me know,

Thanks,

Mark

--
You received this message because you are subscribed to the Google Groups "nltk-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to nltk-users+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Dimitriadis, A. (Alexis)]

I can answer the second part of your question: The nltk is in active development, and I for one haven’t seen any signs of its being replaced by something else in its niche, as a general-purpose Python nlp toolkit. (In fact there are packages like `textblob` that use the nltk behind a thin wrapper of their own API.) 

Anyway it would be great if you were able to fix up the prover. The only reason not to try, that I can see, is if you decide to use another tool (indeed Prover9 was reliable, in my experience, but not the easiest tool to use.) On http://www.nltk.org/contribute.html you can see how to contribute code to the nltk, and also a summary of recent developments, links to the githup repo and bug tracker, etc. 

Best,

Alexis

Dr. Alexis Dimitriadis | Assistant Professor and Senior Research Fellow | Utrecht Institute of Linguistics OTS | Utrecht University | Trans 10, 3512 JK Utrecht, room 2.33 | +31 30 253 65 68 | a.dimi...@uu.nl | www.hum.uu.nl/medewerkers/a.dimitriadis

To unsubscribe from this group and stop receiving emails from it, send an email to nltk-users+...@googlegroups.com.

[Mark Woodward]

Thank you. I may take a crack at it.

Also, I did identify a different problem with skolemize() (https://github.com/nltk/nltk/issues/1701) if anyone wants to take a look at that.

Best,

Mark