IW Meeting 2009-10-01

From Inference Web

Contents 1 agenda 2 notes 2.1 load a proof by URI 2.2 update demo wiki page 2.3 demo 2.4 iwsearch report

• 2009-10-01
• IW Meeting 2009-09-24

agenda

1. Demo - Combine and Improve Proofs

• Cynthia regenerate PUZ001-1 with URIed Information
  • Li has generated some sample normalized PML data (add URI to Information, add triple "pmlr:hasMember") see http://inference-web.org/test/norm

• mini-image in page - svg rendering for each proof: original, improved_self (compare with original), improved_all (compare with original)

• save the improved PML proof in pml2
  • keep several alternatives (current approach)
  • only keep the optimal one (suggested, how do i know which is the best one in the browser?)

• inference rule
  • some inference steps does not have inference rule
  • negated conjecture, it is not direct assertion

• demo script
  • 1. the demo article - Demo - Combine and Improve Proofs
  • 2. a sortable table linking alternative solutions. - similar to http://inference-web.org/tmp/seuReport.html
    • For each inference-engine, we have (a) original; (b) self-improved(p1); (c) root improved(p2); (d) root optimal, (d) global optimal . see Talk:Demo_-_Combine_and_Improve_Proofs#improve_strategy
    • link to SVG image, iwbrowser
  • 3. svg image
    • show the globally combined one - png
    • show individual proof (optimized comparing with original) -
      • improve-self http://inference-web.org/test/combine/PUZ/PUZ001-1/EP---1.1pre/answer_improve_self.svg
      • improve-root http://inference-web.org/test/combine/PUZ/PUZ001-1/EP---1.1pre/answer_improve_root.svg
      • global optimal http://inference-web.org/test/combine/PUZ/PUZ001-1/EP---1.1pre/answer_improve_global.svg
      • Each diamond has a hot link back to the original proof (local-view)
  • 4. a local-view for a nodeset - e.g. http://browser.inference-web.org/iwbrowser/BrowseNodeSet?url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FEP---1.1pre%2Fanswer.owl%23ns_43
    • link to iwbrowser, probeit, tabulator
  • 5. a global iwbrowser view for a nodeset
    • link to local-view
  • 6. a global probeit view for a nodeset
    • link to ?
    • can probeIt be initialized by a uri of nodeset?

2 On Tracking Inference Step Reuse

• goal
  • given two published pml proofs, represent their difference (e.g. did they use the same step, i.e. same input, output, rule)
  • when exporting the optimized proof, also link back to reused fragments of the original proofs

3. iw:Challenges for PML

• goal: identify the limitation of PML in capture and computing provenance

notes

load a proof by URI

load a single proof

1. iwbrowser(global): http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Dag&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftonys%2Ftonys_2%2Fns8.owl%23ns8
2. iwbrowser(proof-view): http://browser.inference-web.org/iwbrowser/NodeSetBrowser?w=900&mg=999&st=Proof&fm=Raw&url=http%3A%2F%2Finference-web.org%2Fproofs%2Ftonys%2Ftonys_2%2Fns8.owl%23ns8
3. iwbrowser(local-view): http://browser.inference-web.org/iwbrowser/BrowseNodeSet?uri=http%3A%2F%2Finference-web.org%2Fproofs%2Ftonys%2Ftonys_2%2Fns8.owl%23ns8
4. iwbrowser(context-view): http://browser.inference-web.org/iwbrowser/ViewContext?uri=http://inference-web.org/proofs/tonys/tonys_2/ns8.owl%23ns8
5. probeIt(global): http://iw.cs.utep.edu:8080/startprobeit/webstart?pmlURI=http%3A%2F%2Finference-web.org%2Fproofs%2Ftonys%2Ftonys_2%2Fns8.owl%23ns8
6. probeIt(local): http://iw.cs.utep.edu:8080/startprobeit/webstart?pmlURI=http%3A%2F%2Finference-web.org%2Fproofs%2Ftonys%2Ftonys_2%2Fns8.owl%23ns8&features=l
7. tabulator: http://dig.csail.mit.edu/2005/ajar/release/tabulator/0.8/tab?uri=http%3A%2F%2Finference-web.org%2Fproofs%2Ftonys%2Ftonys_2%2Fns8.owl%23ns8
8. svg view: http://inference-web.org/test/combine/pml/proofs_tonys_tonys_2_ns8_owl.svg
9. idv view: --http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReply?QuietFlag=-q1&SubmitButton=ProcessSolution&System___IDV---0.0=IDV---0.0&ProblemSource=URL&FormulaURL=http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---1.1pre/combine_P2_combine.tptp

? idv: http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---1.1pre/combine_P2_combine.tptp

load a combined proof

• probeIt(forrest): http://iw.cs.utep.edu:8080/startprobeit/webstart?pmlURI=http%3A%2F%2Finference-web.org%2Fproofs%2Ftptp%2FSolutions%2FPUZ%2FPUZ001-1%2FEP---1.1pre%2Fcombine_P2_combine.owl%23answer
• svg view: http://inference-web.org/test/combine/PUZ/PUZ001-1/combine.svg
• iwbrower(global): 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.2%2Fcombine_P3_self_improve.owl%23answer

update demo wiki page

• put probeIt image on demo page
• get an account for nick on iw wiki

demo

several dimensions for demo

• display
• improvement strategies: self improve
• quality metrics: # of axiom, # of step

statistic table

• (li, cynthia and Geoff) statistics of proof and difference proofs.
• (cynthia) generate statistic table

iwsearch report

• (cynthia, li) Deb need joint report on iwsearch (strength)