# 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.