IW Meeting 2008-11-11

From Inference Web

Jump to: navigation, search

Agenda

Combining Proofs

  • Cynthia's demo and questions (see below) we focuses on the fourth most time
  • Paper writing

What is valid PML

  • James send some examples
  • Paulo want yes/no answer, we may try to eliminate the warnings.

GILA and PML

  • James will generate PML from GILA log
  • James will send the intial draft for ProbeIt to render
  • James will then try to reuse L/M code to generate code to render GILA conclusions, and then get it as a ProbeIt plug-in

Cynthia's demo and question

  • Cynthia has demonstrated some new proofs

1. http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FEP---1.0pre%2Fcombined11.owl%23answer

2. http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FEP---0.999%2Fcombined11.owl%23answer

3.http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FMetis---2.1%2Fcombined11.owl%23answer

4.http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FFaust---1.0%2Fcombined11.owl%23answer

5.http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FVampire---9.0%2Fcombined11.owl%23answer

These are the complete "combined" proofs of PUZ001-1 problem based on "size" combining criteria. The Otter, SNARK, SOS and SPASS proofs were not affected by the combining process.

Some remaining questions:

  • When deciding the size of a proof branch, currently only cnf formula nodesets are counted and fof nodesets are ignored.
    • What about those nodesets created during converting process because of the nested tptp inference?
  • When iwbrowser calculating the size of proof for display, should those fof nodesets be counted?
    • if yes, a combined proof can sometimes have "larger" size than the original.
    • if no, a combined proof can sometimes have smaller size but appear to be larger.
  • PML uses a list of inference steps to capture multiple inference steps. When the combined proof is being converted back to tptp, how can a formula capture multiple sets of parents?


bug and solution

bug

James reported error:

we observed the following from tomcat output

Remote PML Factory Loaded Successfully...
java.lang.ClassCastException: java.lang.String cannot be cast to org.inference_web.pml.context.DataObject
 at org.inference_web.pml.v2.util.PMLObjectManager.loadNodeSet(Unknown Source)
 at org.inference_web.pml.v2.util.PMLObjectManager.getNodeSet(Unknown Source)

solution

  • CSC: At one time, we agreed that we'd use blank nodes for instances of

PMLJ.NodeSetList and some other classes. But g_pml_11.rdf did use named resource for NodeSetList instances and g_pml_10.rdf did not. That is why g_pml_10.rdf was loaded by iwbrowser but not g_pml_11.rdf. It is perfectly legal to use named resource for NodeSetList instances though. I took care of the problem and now you can use:

Personal tools
Navigation