IW Meeting 2009-03-19

From Inference Web

Jump to: navigation, search




metric for quality for ATP

efficiency mode

size: A proof that uses less axioms is better generally;

  • A(1,2,3,4) > B(2,3,4,5,6)

partial order: A proof that uses a subset of the axiom of another is better than that other; (unless there is a subset relation)

  • A(1,2) > B(1,2,3,4,5,6)

discovery mode

uniqueness: A proof that is further away from (all other known proofs) is better.

  • C(1,5,6), A(1,2,3), B(1,2,4), C is better than A or B given A,B,C
  • use the proof has
    • lowest average axiom frequency
    • highest average inverse axiom frequency

non-linear computation, e.g. entropy


  • Geoff will be in benchmarking
  • honglei will reserve a conference room at stanford on wednesday afternoon

meetup at stanford

  • Tuesday morning, after coffee break
  • Wednesday noon lunch and then the afternoon. location gates 260.
Facts about IW Meeting 2009-03-19RDF feed
Date19 March 2009  +
Personal tools