-
-
Notifications
You must be signed in to change notification settings - Fork 4.4k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Fixed PropKB Ask. Added function to check validity. #2830
Conversation
sd-biswas
commented
Jan 25, 2014
- Added function to check for validity of propositional sentences
- Fixed bug where all queries on an empty KB would return False
- Fixed PropKB Ask function to correctly give the logical entailment
- Added Tests for the above
Is there a reason I am unable to give line by line comments? @asmeurer Anyways, some technical stuff-
|
I can't do it either. I think GitHub's javascript must be broken right now. |
|
s = set() | ||
for q in query_conjuncts: | ||
s = s.union(q.atoms(C.Symbol)) | ||
return bool(dpll(query_conjuncts, list(s), {})) | ||
return True if dpll(query_conjuncts, list(s), {}) is False else False |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
You may want to add an inline comment explaining why this is so. We don't want any confusion about the algorithms and logic behind our code, as is the case for most of the logic module as of now.
You may want to bring your function into the sympy.logic namespace by entering it into the init file in sympy.logic folder. Also, I think one of the tests in test_PropKB is failing. Please look into that and fix the issue. |
|
This seems to be fine now. I am assuming you have tested all the test cases by hand and confirmed their validity. |
|
||
|
||
|
||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I think, 2 newlines enough...
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
+1. @SDB1323 , have one newline between methods of a class, and two newlines between module-level functions/classes.
Travis seems to be giving the following error: Could someone please indicate whether some action is required from my side, or it is normal to get this message and the PR will be merged? |
Ping @skirpichev |
Travis is timing out a lot these days. I'm not sure what the major issue is. |
timeouts in test_gruntz.py/test_wester.py should be rare after merging #2851 |
I haven't reviewed it, but if you are OK with the changes, then please merge. |
Could this PR be merged? I need the valid function for a future PR. Travis passes all but one test, which times out. |
I am really sorry. But all my ways to make Travis rebuild failed. And since most of the tests had timed out there was no way to know whether the build was correct or not. Hence the desperate attempt. I apologize. |
@SDB1323, can you rebase this pr to get rid of meaningless commits? |
@@ -92,6 +93,30 @@ def satisfiable(expr, algorithm="dpll2"): | |||
raise NotImplementedError | |||
|
|||
|
|||
def valid(expr): | |||
""" | |||
Check validity of a propositional sentence. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Does valid mean tautological? If so, I think that "tautological" is a better word to use here.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I guess "valid" is more used in logic, though https://en.wikipedia.org/wiki/Valid. It should be made clear in the docstring what this means, though, in case someone isn't familiar with the logic terminology.
I think Travis failed because of some old test failure from two months ago. Once you push commits addressing my comments, that should go away. |
if isinstance(expr, bool): | ||
return expr | ||
|
||
if satisfiable(Not(expr)) is False: |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
return not satisfiable(Not(expr))
My main concern here is the changed test cases for kb.ask. What does that function do? Can you explain why the previous test cases were wrong? |
This needs to be merged with master. |
@asmeurer I have fixed the merge conflicts as well as added a couple of pending things. Please review. |
.. [1] en.wikipedia.org/wiki/Validity | ||
|
||
""" | ||
if isinstance(expr, bool): |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This shouldn't be needed.
@asmeurer : This seems to have passed the Travis build. Please review and merge if no further changes are required. The last commit should fix the {false: true} mapping problem, along with the python 2.6 compatibility fix. |
Did you add a test for the {false: true} issue? |
Fixed PropKB Ask. Added function to check validity.