EProver seems to not working in the apease/sigmakee2018:latest docker, and new docker fails to build #76
Comments
|
The Docker version of SigmaKEE is very out of date at this point (since 2018) and I haven't been maintaining it. I recommend the 'native' install of SigmaKEE as described in the README. There's a video that can help at https://www.youtube.com/watch?v=ZVW0WllvoUU&t=3s&ab_channel=OntologyTalkwithAdamPease |
|
@apease thank you for your answer. Indeed native installation works and I've managed to run reasoning via Ask/Tell interface, but only with Vampire, for some reason the EProver option is gray. In README is written that Ask/Tell interface is not well maintained, so there are two questions:
|
|
Hi Sergey
I'm travelling today so I hope to respond in detail tomorrow. Eprover should work with sigma, I'll try to replicate. The tests directory in the sigma repository should provide some more complex examples of reasoning problems.
All the best
Adam
On Nov 3, 2022 11:19 AM, Sergey Rodionov ***@***.***> wrote:
@apease<https://github.com/apease> thank you for your answer. Indeed native installation works and I've managed to run reasoning via Ask/Tell interface, but only with Vampire, for some reason the EProver option is gray. In README is written that Ask/Tell interface is not well maintained, so there are two questions:
1. What would be the most "canonical" way to run reasoning in the case when there is an addition to the knowledge base. For example we want to add some "individuals" and make reasoning about them?
2. Where would be the best place to find some practical examples of relatively complex reasoning with SUMO ontology?
—
Reply to this email directly, view it on GitHub<#76 (comment)>, or unsubscribe<https://github.com/notifications/unsubscribe-auth/AAQG6HKT4TR3QP6JDS5YEK3WGONUBANCNFSM6AAAAAARTHKHF4>.
You are receiving this because you were mentioned.Message ID: ***@***.***>
|
|
Hi Adam! Actually the part of the problem with EProver was because of wrong path to EProver in However, even after this fix, EProver doesn't seem to work. For the following call : return the following (I will post the whole output just in case) |
|
Hi Sergey, Yes, as per the README every occurance of 'theuser' needs to be changed to conform to your username/path . But there appears to be an issue that the tptp file isn't getting generated and so the theorem provers have no content to prove on, at least on my installation. I'm worried I might have uploaded a test version that turned off inference. I'm researching this and hope to respond soon. |
|
Hi Sergey, I'm not sure what's causing the issue at the moment. Recently, I've been just generating TPTP FOF (of TFF or TFF) from Sigma's command line interface, then running provers directly. It has a shorter workflow than doing things from the GUI. For example /home/apease/workspace/vampire/vampire --proof tptp -t 30 /home/apease/.sigmakee/KBs/SUMOedited.tptp Vampire generally is doing better than E for fof queries in recent versions |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
There are two possible problems:
It seems that in apease/sigmakee2018:latest docker EProver is not working (and actually all other proposed reasoners). However it well might be that I'm not using it correctly. I connected to the server (http://localhost:8080/) and went to Ask/Tell menu. Proposed example query
(instance ?X Relation)returns nothing. I've also tried the following:(query (equal 13 (MultiplicationFn 3 4))). It also returns nothing.I've tried to rebuild docker (In order to check reasoner in the master), but it fails with the following message:
The text was updated successfully, but these errors were encountered: