IW Meeting 2008-12-16

From Inference Web

Jump to: navigation, search

Contents

agenda

  • combine proof
  • pml validator (Jiao is away)

IW Meeting 2008-12-9

notes

PML back to TPTP

demo (require Java 1.5 or up, Firefox, XP)

  1. go to http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTSTP
  2. check a radio button followed by text "URL to fetch from"
  3. paste a URL in the textarea below the radio button: http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Vampire---9.0/combined11.tptp
  4. check a checkbox followed by text "IDV 0.0"
  5. click button "processSolution"

The configuration should look like the following Image:TPTP Display Configure.png

you should expect to see a Java browser with the following display. Note that the proof is combined from multiple Proofs in PML and translated back to TPTP. Image:TPTP Combined Proof in TPTP Viewer.gif

more examples

Equality Semantics

Geoff has several approaches, Cynthia is using one

Metrics for combine

Quality: Size (number of inferenceSteps in DAG), Max depth, Subsumption, Average branching (min), Average branching (max). All metrics are wrt the CNF part of the proofs.

tractable : smaller proof

  • minimize the number of nodes in the final combined proof
  • minimize the number of leave nodes
  • minimize the depth of proof (less long argument)

trust: proof coming from multiple sources

  • diversity metric: justify proofs by many different sources, different inference engines, in many different ways, connectivity
  • full expansion: expand tree node as much as possible

current approach

1. translate tptp to pml

  • 98% done
  • cleanup and backup code

2. compute equality

  • we have switched from string comparision to FOL formula comparision (provided by Geoff)


3. combine proof

3.1. global with normalization (optional)

  • each normalized-structure is one step sub-proof (corresponding to one inference step)

3.2 greedy

  • breadth-first traverse the given proof, for each node in the proof, try to find the best justification to that node (we have alternatives base node equavlence form other proofs), only keep the best justification (PML can keep both original and the best), and continue until no more work
Retrieved from "http://inference-web.org/wiki/IW_Meeting_2008-12-16"
Personal tools
Navigation