IW Meeting 2008-12-09

From Inference Web

Jump to: navigation, search

agenda

  • jiao introduction
  • pml validator (5min) jiao, cynthia
  • combine proof, geoff, cynthia
  • combine proof (optimize), honglei, and li

notes

pml validator: Jiao put one more example about subproperty mentioned by Cynthia on tw wiki. About the wiki log example, it will be put later on wiki Everybody's opinion is needed about the items in "what is a valid pml validator?"

combine proof

cnf(Vampire---9.0_39,negated_conjecture,
   ( $false ),
   inference('resolution, forward subsumption resolution',[],[Vampire---9.0_7,Vampire---9.0_10,Vampire---9.0_38])).
...

cnf(Vampire---9.0_37,negated_conjecture,
   ( hates(butler,butler) ),
   inference('resolution, forward subsumption resolution',[],[SNARK---20070805r043_different_hates,SNARK---20070805r043_17,SNARK---20070805r043_agatha_hates_agatha])).

...
cnf(Vampire---9.0_38,negated_conjecture,
   ( ~ hates(butler,agatha) ),
   inference(resolution,[],[Vampire---9.0_29,Vampire---9.0_37])).
...
cnf(SNARK---20070805r043_different_hates,hypothesis,
   ( ~ hates(agatha,X)
   | ~ hates(charles,X) ),
   file('PUZ001-1.tptp',different_hates)).


honglei

1. Definition of proof-combine and unified notations
2. An outline of Brute-force global approach
3. Benchmark (global vs. local)
4. Future direction?

action items


  • cynthia update combine proof by adding single quotes around formula names.

Rather

 cnf(Vampire---9.0_39,negated_conjecture,
  ( $false ),
  inference('resolution, forward subsumption resolution',[],[Vampire---9.0_7,Vampire---9.0_10,Vampire---9.0_38])).

Use

 cnf('Vampire---9.0_39',negated_conjecture,
   ( $false ),
   inference('resolution, forward subsumption resolution',[],['Vampire---9.0_7','Vampire---9.0_10','Vampire---9.0_38'])).
  • geoff is planning to browse the combined proof using his Viz tool.
  • Cynthia make changes: Use the inference rule from the replacING NodeSet in the TPTP inference() record. (Not the inference rule from the replacED NodeSet.)


  • metrics
    • geoff has contributed five metrics
    • paulo will contribute one metric
  • honglei, Li, and geoff
    • clarify notation
    • problem description and metrics, the properties of metrics (local minimal may lead to greedy)
    • brute-force global optimization


  • we will have the next meeting, paulo and deb will be in AGU
Personal tools
Navigation