IW Meeting 2009-03-19
From Inference Web
2009-03-19
Contents |
agenda
- review IW Meeting 2009-03-12
- review Combine proof example 1
- review Combine proof example 2
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
actions
- 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.
