Problem in using nullary predicate (ie propositional) symbols for tableau and resolution provers

[alexrudnick]

What steps will reproduce the problem?

>>> import nltk
>>> from nltk.sem import logic
>>> lp = logic.LogicParser()
>>> con = lp.parse('(P & -P)')
>>> con
<AndExpression (P & -P)>
>>> from nltk.inference import *
>>> get_prover(con, [], prover_name='Prover9').prove()
False
>>> get_prover(con, [], prover_name='tableau').prove()
>>> get_prover(con, [], prover_name='resolution').prove()

What is the expected output? What do you see instead?

should get False, False, False.
The call to Prover9 returns False, but the other two raise errors:

File "/Users/ewan/svn/nltktrunk/nltk/nltk/test/tp-temp.doctest", line 10,
in tp-temp.doctest
Failed example:
get_prover(con, [], prover_name='tableau').prove()
Exception raised:
Traceback (most recent call last):
File
"/System/Library/Frameworks/Python.framework/Versions/2.5/lib/python2.5/doctest.py",
line 1212, in __run
compileflags, 1) in test.globs
File "<doctest tp-temp.doctest[7]>", line 1, in <module>
File "/Library/Python/2.5/site-packages/nltk/inference/api.py", line
266, in prove
verbose)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py",
line 32, in prove
result = _attempt_proof(agenda, set(), set(), debugger)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py",
line 196, in _attempt_proof
return proof_method(current, agenda, accessible_vars, atoms, debug)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py",
line 303, in _attempt_proof_n_and
agenda.put(-current.term.first)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py",
line 79, in put
self.sets[self._categorize_expression(ex_to_add)].add(ex_to_add)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py",
line 135, in _categorize_expression
return self._categorize_NegatedExpression(current)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py",
line 166, in _categorize_NegatedExpression
raise ProverParseError()
ProverParseError

---

File "/Users/ewan/svn/nltktrunk/nltk/nltk/test/tp-temp.doctest", line 11,
in tp-temp.doctest
Failed example:
get_prover(con, [], prover_name='resolution').prove()
Exception raised:
Traceback (most recent call last):
File
"/System/Library/Frameworks/Python.framework/Versions/2.5/lib/python2.5/doctest.py",
line 1212, in __run
compileflags, 1) in test.globs
File "<doctest tp-temp.doctest[8]>", line 1, in <module>
File
"/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 107,
in prove
verbose)
File
"/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 40,
in prove
clauses.extend(clausify(-goal))
File
"/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 418,
in clausify
for clause in _clausify(skolemize(expression)):
File
"/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 486,
in skolemize
return to_cnf(skolemize(-negated.first, univ_scope),
File
"/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 509,
in skolemize
raise ProverParseError()
ProverParseError

Please use labels and text to provide additional information.

Migrated from http://code.google.com/p/nltk/issues/detail?id=138

---

earlier comments

ewan.klein said, at 2008-12-15T14:08:51.000Z:

I'm now getting a different error, which is similar to the problem I had with the Cooper storage parsing, and seems to be due to the use of isinstance() tripping over the non-qualified class.

from nltk.inference import *
get_prover(con, [], prover_name='tableau').prove()
Traceback (most recent call last):
File "/Users/ewan/svn/nltktrunk/", line 1, in
File "/Library/Python/2.5/site-packages/nltk/inference/api.py", line 266, in prove
verbose)
File "/Library/Python/2.5/site-packages/nltk/inference/tableau.py", line 40, in prove
agenda.put(-goal)
File "/Users/ewan/svn/nltktrunk/", line 351, in neg
File "/Library/Python/2.5/site-packages/nltk/sem/logic.py", line 957, in init
assert isinstance(term, Expression), "%s is not an Expression" % term
AssertionError: (P & -P) is not an Expression
get_prover(con, [], prover_name='resolution').prove()
Traceback (most recent call last):
File "/Users/ewan/svn/nltktrunk/", line 1, in
File "/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 107, in
prove
verbose)
File "/Library/Python/2.5/site-packages/nltk/inference/resolution.py", line 52, in
prove
clauses.extend(clausify(-goal))
File "/Users/ewan/svn/nltktrunk/", line 351, in neg
File "/Library/Python/2.5/site-packages/nltk/sem/logic.py", line 957, in init
assert isinstance(term, Expression), "%s is not an Expression" % term
AssertionError: (P & -P) is not an Expression

DHGarrette said, at 2008-12-21T10:32:49.000Z:

Fixed for Tableau prover. Still working on resolution prover.

[stevenbird]

Closing; too old