IW Meeting 2009-04-02

From Inference Web

Jump to: navigation, search

2009-04-02

agenda

  • previous meeting: IW Meeting 2009-03-24
    • mizar proof, clean up translation problems in newton (cynthia, geoff)
    • generate one conclusion mapping file (pairs of conclusions which are the same) for each problem (cynthia)
    • realize the metrics in combine algorithm (li)
    • soundness of this approach (honglei)

notes

mizar proof

benefit of TPTP-PML translation

  • During TPTP-PML translation, we've found some dangling fragments in proofs (we see a forest but not a DAG)
  • cynthia has combine the forest into a DAG

cynthia's mapping files

http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/EP---1.0/equalNS.owl
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Faust---1.0/equalNS.owl
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Metis---2.1/
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Otter---3.3/equalNS.owl
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SNARK---20080805r005/equalNS.owl
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SOS---2.0/equalNS.owl
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/SPASS---3.01/equalNS.owl
http://inference-web.org/proofs/tptp/Solutions/PUZ/PUZ001-1/Vampire---9.0/equalNS.owl

li's combine proof


honglei's complexity analysis: "sharp P"

Image:combine-proof-complexity-200904.jpg

action

  • (geoff) will work on the jaccard metrics
  • (honglei and Li) will work on the complexity analysis
  • (Li) work out the first ATP combine problem
  • for the next week Deb and Li will be in-transit
  • (cynthia) work on mizar translation, and update ATP proofs
Facts about IW Meeting 2009-04-02RDF feed
Date2 April 2009  +
Personal tools
Navigation