search

ontologyportal / sigmakee

Sigma Knowledge Engineering Environment
https://www.ontologyportal.org
GNU General Public License v3.0
103 stars 35 forks source link

Can't run "Consistency Check" #2

Open fcbr opened 8 years ago

fcbr commented 8 years ago

After booting up SIGMAKEE, select "Consitency Check" and keep the defaults (EProver).

Problem: it doesn't seem to work and we get the following exception on the console:

Feb 18, 2016 2:06:30 PM TPTPWorld.InterfaceTPTP init
INFO: Initializing InterfaceTPTP.
Feb 18, 2016 2:06:33 PM TPTPWorld.InterfaceTPTP init
INFO: Initializing InterfaceTPTP.

INFO in EProver.submitQuery() conjecture: fof(conj1,conjecture, (
s__instance(s__instance__m,s__BinaryPredicate) )).

Get response from EProver, start for parsing ...
Feb 18, 2016 2:06:34 PM com.articulate.sigma.CCheckManager
performConsistencyCheck
INFO: KB SUMO has been added to the queue for consistency check.
INFO in KB.addConstituent(): /home/fcbr/repos/sumo/KBs/emptyConstituent.txt
.INFO in KB.addConstituent(): added 1 formulas and 2 terms.
null
null
null
null
null
java.lang.NullPointerException
        at com.articulate.sigma.PredVarInst.hasCorrectArityRecurse(PredVarInst.java:130)
        at com.articulate.sigma.PredVarInst.hasCorrectArity(PredVarInst.java:185)
        at com.articulate.sigma.KB.tell(KB.java:1500)
        at com.articulate.sigma.CCheck.runConsistencyCheck(CCheck.java:361)
        at com.articulate.sigma.CCheck.run(CCheck.java:428)
        at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1142)
        at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:617)
        at java.lang.Thread.run(Thread.java:745)
apease commented 8 years ago

Hi Fabricio, Still tracking this down - I've fixed some apparent problems where fixes this past spring to the TPTP translation apparently didn't accommodate cases of nearly empty KBs, such as when we start with an empty KB and add statements one at a time for consistency checking. But the more stubborn issue is that I'm not getting responses from the process that communicates with E. I'll upload my (partial) fixes later today in case you want to see the behavior.

Adam

On 02/19/2016 08:37 AM, Fabricio Chalub wrote:

After booting up SIGMAKEE, select "Consitency Check" and keep the defaults (EProver).

Problem: it doesn't seem to work and we get the following exception on the console:

|Feb 18, 2016 2:06:30 PM TPTPWorld.InterfaceTPTP init INFO: Initializing InterfaceTPTP. Feb 18, 2016 2:06:33 PM TPTPWorld.InterfaceTPTP init INFO: Initializing InterfaceTPTP. INFO in EProver.submitQuery() conjecture: fof(conj1,conjecture, ( sinstance(sinstancem,sBinaryPredicate) )). Get response from EProver, start for parsing ... Feb 18, 2016 2:06:34 PM com.articulate.sigma.CCheckManager performConsistencyCheck INFO: KB SUMO has been added to the queue for consistency check. INFO in KB.addConstituent(): /home/fcbr/repos/sumo/KBs/emptyConstituent.txt .INFO in KB.addConstituent(): added 1 formulas and 2 terms. null null null null null java.lang.NullPointerException at com.articulate.sigma.PredVarInst.hasCorrectArityRecurse(PredVarInst.java:130) at com.articulate.sigma.PredVarInst.hasCorrectArity(PredVarInst.java:185) at com.articulate.sigma.KB.tell(KB.java:1500) at com.articulate.sigma.CCheck.runConsistencyCheck(CCheck.java:361) at com.articulate.sigma.CCheck.run(CCheck.java:428) at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1142) at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:617) at java.lang.Thread.run(Thread.java:745) |

— Reply to this email directly or view it on GitHub https://github.com/ontologyportal/sigmakee/issues/2.

Adam Pease http://www.ontologyportal.org http://www.articulatesoftware.com http://www.adampease.org

apease commented 8 years ago

getting closer -it appears e_ltb_runner slightly changed its interface, I've uploaded the latest code, now it's just bugs of assuming a full kbCache to iron out...

On 02/19/2016 03:04 PM, Adam Pease wrote:

Hi Fabricio, Still tracking this down - I've fixed some apparent problems where fixes this past spring to the TPTP translation apparently didn't accommodate cases of nearly empty KBs, such as when we start with an empty KB and add statements one at a time for consistency checking. But the more stubborn issue is that I'm not getting responses from the process that communicates with E. I'll upload my (partial) fixes later today in case you want to see the behavior.

Adam

On 02/19/2016 08:37 AM, Fabricio Chalub wrote:

After booting up SIGMAKEE, select "Consitency Check" and keep the defaults (EProver).

Problem: it doesn't seem to work and we get the following exception on the console:

|Feb 18, 2016 2:06:30 PM TPTPWorld.InterfaceTPTP init INFO: Initializing InterfaceTPTP. Feb 18, 2016 2:06:33 PM TPTPWorld.InterfaceTPTP init INFO: Initializing InterfaceTPTP. INFO in EProver.submitQuery() conjecture: fof(conj1,conjecture, ( sinstance(sinstancem,sBinaryPredicate) )). Get response from EProver, start for parsing ... Feb 18, 2016 2:06:34 PM com.articulate.sigma.CCheckManager performConsistencyCheck INFO: KB SUMO has been added to the queue for consistency check. INFO in KB.addConstituent(): /home/fcbr/repos/sumo/KBs/emptyConstituent.txt .INFO in KB.addConstituent(): added 1 formulas and 2 terms. null null null null null java.lang.NullPointerException at com.articulate.sigma.PredVarInst.hasCorrectArityRecurse(PredVarInst.java:130)

at com.articulate.sigma.PredVarInst.hasCorrectArity(PredVarInst.java:185) at com.articulate.sigma.KB.tell(KB.java:1500) at com.articulate.sigma.CCheck.runConsistencyCheck(CCheck.java:361) at com.articulate.sigma.CCheck.run(CCheck.java:428) at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1142)

at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:617)

at java.lang.Thread.run(Thread.java:745) |

— Reply to this email directly or view it on GitHub https://github.com/ontologyportal/sigmakee/issues/2.

Adam Pease http://www.ontologyportal.org http://www.articulatesoftware.com http://www.adampease.org

apease commented 8 years ago

Hi Folks, It looks like revisions in 2015 to consistency check were not done correctly - the routine is using the KIF source and processing statements one by one into TPTP. Instead, it needs to process all the statements into TPTP first, since that relies on many mutually supporting definitions to get the translation right. Then the routine can submit the TPTP formulas one by one for checking. I'll work on that, but I'm not sure how long it will take.

Adam

On 02/19/2016 08:58 PM, Adam Pease wrote:

getting closer -it appears e_ltb_runner slightly changed its interface, I've uploaded the latest code, now it's just bugs of assuming a full kbCache to iron out...

On 02/19/2016 03:04 PM, Adam Pease wrote:

Hi Fabricio, Still tracking this down - I've fixed some apparent problems where fixes this past spring to the TPTP translation apparently didn't accommodate cases of nearly empty KBs, such as when we start with an empty KB and add statements one at a time for consistency checking. But the more stubborn issue is that I'm not getting responses from the process that communicates with E. I'll upload my (partial) fixes later today in case you want to see the behavior.

Adam

On 02/19/2016 08:37 AM, Fabricio Chalub wrote:

After booting up SIGMAKEE, select "Consitency Check" and keep the defaults (EProver).

Problem: it doesn't seem to work and we get the following exception on the console:

|Feb 18, 2016 2:06:30 PM TPTPWorld.InterfaceTPTP init INFO: Initializing InterfaceTPTP. Feb 18, 2016 2:06:33 PM TPTPWorld.InterfaceTPTP init INFO: Initializing InterfaceTPTP. INFO in EProver.submitQuery() conjecture: fof(conj1,conjecture, ( sinstance(sinstancem,sBinaryPredicate) )). Get response from EProver, start for parsing ... Feb 18, 2016 2:06:34 PM com.articulate.sigma.CCheckManager performConsistencyCheck INFO: KB SUMO has been added to the queue for consistency check. INFO in KB.addConstituent(): /home/fcbr/repos/sumo/KBs/emptyConstituent.txt .INFO in KB.addConstituent(): added 1 formulas and 2 terms. null null null null null java.lang.NullPointerException at com.articulate.sigma.PredVarInst.hasCorrectArityRecurse(PredVarInst.java:130)

at com.articulate.sigma.PredVarInst.hasCorrectArity(PredVarInst.java:185) at com.articulate.sigma.KB.tell(KB.java:1500) at com.articulate.sigma.CCheck.runConsistencyCheck(CCheck.java:361) at com.articulate.sigma.CCheck.run(CCheck.java:428) at java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1142)

at java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:617)

at java.lang.Thread.run(Thread.java:745) |

— Reply to this email directly or view it on GitHub https://github.com/ontologyportal/sigmakee/issues/2.

Adam Pease http://www.ontologyportal.org http://www.articulatesoftware.com http://www.adampease.org

arademaker commented 8 years ago

Adam,

It seems that we found a perfect opportunity for collaboration. Do you have any paper that describes the transformation from SUMO to TPTP? If you don't have, would you mind starting by explaining the intentional behaviour of the transformation before digging into the code? That way, we may help from our side. I am especially interesting in not embedded ways to call E Prover. That is, I would like a transformation that generates the TPTP files only from the KIF files, leaving the user to call E Prover directly.

Best,

Alexandre Rademaker http://arademaker.gtihub.com

On Feb 21, 2016, at 12:24 PM, Adam Pease notifications@github.com wrote:

Hi Folks, It looks like revisions in 2015 to consistency check were not done correctly - the routine is using the KIF source and processing statements one by one into TPTP. Instead, it needs to process all the statements into TPTP first, since that relies on many mutually supporting definitions to get the translation right. Then the routine can submit the TPTP formulas one by one for checking. I'll work on that, but I'm not sure how long it will take.

Adam

arademaker commented 8 years ago

BTW, is this issue related with both #4 and #3 right?

apease commented 8 years ago

Hi Alexandre, My book explains it, but you can also find that content in

Pease, A., Schulz, S., (2014). Knowledge Engineering for Large Ontologies with Sigma KEE 3.0, in Proceedings of IJCAR-2014. http://www.adampease.org/professional/pe_sch_sigma.pdf

That transformation is com.articulate.sigma.SUMOKBtoTPTPKB. But I do hope that we don't create any new code that isn't part of Sigma. There's lots of existing support in the code for this sort of thing and doing something external, although it might appear simpler at first, will just likely cause duplication as well as divergence.

Adam

apease commented 8 years ago

yes

apease commented 8 years ago

Hi Alexandre, I'm rewriting com.articulate.sigma.CCheck.runConsistencyCheck. This will also require rewriting several other routines in CCheck so that they pass TPTP directly to the provers (which also include the SInE meta-prover in Sigma and LEO-II) as well as handling the proof response directly, rather than passing them through the SUO-KIF-based com.articulate.sigma.KB object. Let me know if you folks want to be involved in that.

Adam