IW Meeting 2009-05-14

From Inference Web

Jump to: navigation, search

Contents

agenda

  • note new call in info using free telecon:
    • Conference Dial-in Number: (605) 475-4850
    • Participant Access Code: 852017#
    • Host Access Code: 852017*
  • combine
    • Cynthia's results
    • Li's results
      • proof quality metric
    • honglei's results
  • provenance challenge
    • paulo's result
  • iwsearch - halted to finish combined proof


  • two added issues
    • pml validator
    • update PML ontology to support tracking provenance of combined proof

notes

pml validator

  • Li will transfer the work to cynthia
  • we will not only check the syntax as we did, we will also check the semantics (e.g. if the proof contains cycle)

cynthia's results

I have produced a set of pml proofs for the "agatha" tptp problem, with each proof has a root NodeSet to answer the "agatha" query. These proofs are what I call "fully combined" proofs, which means any possible derivation to proof the "agatha" problem is in there. For any tptp formula in this problem's solutions, if there is an "equal" formula, the NodeSets for these formulae are combined, except the specific rules we have set so far. These proofs should represent the answer to Paulo's question of "how many different proofs can be produced?" If you use the browser to look through the proofs, by clicking any "<" or ">" symbol, you get a different derivation. Each derivation can be considered as a "view" of the complete proof set, as Paulo mentioned before. Based on this complete proof set, you can extract different derivations using different criteria. For example, Geoff and I use "find smallest inference step" criterion to produce some derivations, and Li uses others.

I think I can also calculate the total number of derivations for each proof: total number of derivations = NodeSet1(# of inference steps) x NodeSet2(# of inference steps) x ... x NodeSetn(# of inference steps) I have not tried this yet, and need you to verify.

Here are the links to these proofs:

PML ontology update

  • purpose: track provenance of combined proofs
  • Paulo's proposal
    • change cardinality
    • add hasOriginalProof (not sure about the name)
  • Li's proposal: recommend some PML files to be free of blank node

Li's results

performance

linked justifications (linked to iwbrowser)


example combined result

algorithm context_lg problem solution axioms axioms(cnf) nodes nodes(cnf) root_uri_browser finish process_time(sec) solution_cnt
original original PUZ001-1 SOS---2.0 10 10 17 17 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SOS---2.0/answer.owl#answer
- - -
original original PUZ001-1 Metis---2.1 10 10 38 38 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Metis---2.1/answer.owl#answer
- - -
original original PUZ001-1 EP---0.999 10 10 23 23 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---0.999/answer.owl#answer
- - -
original original PUZ001-1 Ayane---1.1 10 10 21 21 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Ayane---1.1/answer.owl#answer
- - -
original original PUZ001-1 SNARK---20080805r005 10 10 17 17 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SNARK---20080805r005/answer.owl#answer
- - -
original original PUZ001-1 EP---1.0 10 10 23 23 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---1.0/answer.owl#answer
- - -
original original PUZ001-1 Metis---2.2 10 10 38 38 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Metis---2.2/answer.owl#answer
- - -
original original PUZ001-1 Otter---3.3 10 10 17 17 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Otter---3.3/answer.owl#answer
- - -
original original PUZ001-1 Vampire---9.0 10 10 21 21 ">http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Vampire---9.0/answer.owl#answer
- - -
traverse combined PUZ001-1 SOS---2.0 12 12 29 29 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/SOS---2.0.combined.traverse.combine1.owl#id00201
ok 5.205 6860
axiom_node_cnf3 combined PUZ001-1 SOS---2.0 10 10 17 17 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/SOS---2.0.combined.axiom_node_cnf3.combine1.owl#id00201
ok 2.726 25
traverse combined PUZ001-1 Metis---2.1 12 12 33 33 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Metis---2.1.combined.traverse.combine1.owl#id00111
ok 7.681 6860
axiom_node_cnf3 combined PUZ001-1 Metis---2.1 10 10 25 25 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Metis---2.1.combined.axiom_node_cnf3.combine1.owl#id00111
ok 3.705 31
traverse combined PUZ001-1 EP---0.999 10 10 23 23 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/EP---0.999.combined.traverse.combine1.owl#id00142
ok 0.0010 1
axiom_node_cnf3 combined PUZ001-1 EP---0.999 10 10 23 23 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/EP---0.999.combined.axiom_node_cnf3.combine1.owl#id00142
ok 0.0020 2
traverse combined PUZ001-1 Ayane---1.1 12 12 22 22 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Ayane---1.1.combined.traverse.combine1.owl#id00181
ok 7.91 15680
axiom_node_cnf3 combined PUZ001-1 Ayane---1.1 10 10 19 19 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Ayane---1.1.combined.axiom_node_cnf3.combine1.owl#id00181
ok 3.774 45
traverse combined PUZ001-1 SNARK---20080805r005 12 12 19 19 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/SNARK---20080805r005.combined.traverse.combine1.owl#id00173
ok 1.332 3920
axiom_node_cnf3 combined PUZ001-1 SNARK---20080805r005 10 10 17 17 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/SNARK---20080805r005.combined.axiom_node_cnf3.combine1.owl#id00173
ok 1.12 37
traverse combined PUZ001-1 EP---1.0 11 11 29 29 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/EP---1.0.combined.traverse.combine1.owl#id00038
ok 9.947 13720
axiom_node_cnf3 combined PUZ001-1 EP---1.0 10 10 18 18 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/EP---1.0.combined.axiom_node_cnf3.combine1.owl#id00038
ok 6.163 51
traverse combined PUZ001-1 Metis---2.2 12 12 33 33 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Metis---2.2.combined.traverse.combine1.owl#id00066
ok 5.702 6860
axiom_node_cnf3 combined PUZ001-1 Metis---2.2 10 10 25 25 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Metis---2.2.combined.axiom_node_cnf3.combine1.owl#id00066
ok 2.721 31
traverse combined PUZ001-1 Otter---3.3 12 12 19 19 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Otter---3.3.combined.traverse.combine1.owl#id00024
ok 1.325 3920
axiom_node_cnf3 combined PUZ001-1 Otter---3.3 10 10 17 17 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Otter---3.3.combined.axiom_node_cnf3.combine1.owl#id00024
ok 1.064 37
traverse combined PUZ001-1 Vampire---9.0 11 11 19 19 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Vampire---9.0.combined.traverse.combine1.owl#id00013
ok 0.023 80
axiom_node_cnf3 combined PUZ001-1 Vampire---9.0 10 10 19 19 ">http://plato.cs.rpi.edu/iw/hypergraph/combine200905-false/PUZ001-1/Vampire---9.0.combined.axiom_node_cnf3.combine1.owl#id00013
ok 0.02 17

Paulo's results

We did generate a SAW (semantic abstract workflow) for the third provenance challenge and used the SAW to generate PML wrappers. The wrappers, however, had to be slightly modified to address the challenge. More specifically, we had to address the following details: how to encode two inference steps without intermediate (this is similar to what Cynthia has done to encode some TPTP solutions); and how a node set can refer to an entire folder as a conclusion. Both problems are being addressed at the wrapper level without any need to change PML2 and we should be done today.

We anticipate that our PML encoding can answer questions 1 and 2. Please let me know how you want to proceed with this conversation. I suggest that a meeting to compare our PML encodings (I anticipate that our encodings are going to be different).

complexity

complexity

  • change "acyclic" to "at least one axiom"

connection with LP, Propositional Horn

  • we have examples, not blind search
  • we use proofs from different sources
  • we use different measures

todo

Personal tools
Navigation