IW Meeting 2009-10-01

From Inference Web

Jump to: navigation, search

Contents

agenda

1. Demo - Combine and Improve Proofs

  • Cynthia regenerate PUZ001-1 with URIed Information
  • 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


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

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)
Personal tools
Navigation