add "or false" to a definition breaks it.
The following theory admits the solution that jerry shaves himself.
!x y: Shaves(x, y) <- (x=jerry & y=jerry).
If I add " | false " at the end of the definition, jerry does not shave himself anymore !?
Yet, a | false is always the same as a (even in ternary logic).
Comments (15)
-
reporter -
probably duplicate of Issue
#953which was incorrectly marked resolved -
@Pierre: it is probably safer to use a subtype of string instead of constructed types while there is no new release. The theory would then look like this: http://dtai.cs.kuleuven.be/krr/idp-ide/?src=be4c034584ba1b75e3dec044602f66fe
-
reporter Thanks for the quick reply. I'll try the work-around in my real problem.
-
If you build IDP yourself, you can also try the fixed version (commit 53b93a0b9b351f2363103de8835d1ee1f01d2309 )
-
I can confirm that all your examples work well in the fixed version.
-
reporter Good to know. Unfortunately, I don't have access to the source code of idp.
-
Now you should be able to access it.
-
reporter Indeed. Thanks.
Before I try to compile idp on a Windows machine (not sure if it is easy), could you tell me if you can solve this theory with it ? The previous version could not find a solution, even after 10 hours of trying...
-
reporter And if you can solve it, could you send me the result ?
-
Hi Pierre,
Some remarks:
-
The bug you had should not be present on Windows version of IDP, only on unix versions (as XSB does not work under windows). So, there's no need to resort to the fix if you run on a windows machine.
-
If you wish to compile IDP on windows, you should ask @ingdas
-
The last theory you sent me does not contain definitions, hence has nothing to do with the current bug
-
The problem with your last theory is that you ask all models and there just are a lot of them. On my machine, if I just ask 10.000 models, I can find (and print) them in 6 seconds. To get some models, see http://dtai.cs.kuleuven.be/krr/idp-ide/?src=d90a32f2cae7d62036bab7b6d5091842
-
-
edit: The estimated number of models of your theory is someting like 2^4 * 2^4 * 2^4 * 2^4 = 65536 (interpretations for
authorizesT(Person, Person) blocksT(Person, Person) authorizesF(Person, Person) blocksF(Person, Person)
Checked this, and there are 44464 of them.
-
reporter OK. Thanks.
-
- changed status to resolved
Merged in graphbug (pull request #414)
Fixed XSB graphing bug. Fixes
#953Fixes#954→ <<cset 2e889d256f0c>>
-
The latest release of IDP contains these fixes. https://dtai.cs.kuleuven.be/krr/files/releases/idp/idp-linux-latest.tar.gz
- Log in to comment
A related, and more significant issue, is that this theory is equivalent to this one (which uses a "or" in the definition, but they yield different results : the first one has no solution (OK), but the second one has one (not OK).