IW Meeting 2008-10-16

proof combination and optimization (CSC)

by combining proofs, a justification tree can generate many possible proofs for the same conclusion
proof optimization: choose the optimized proof from candidates of a justification tree
- proof ordering: before merging, we may generate total order for each proof using a metrics, e.g. # of nodes in proof
- when merging proof, we only keep the original proof and add the "optimal" proof which has the highest order rating.

Original Proof

Optimal Proof

paper call

paper outline (suggested by geoff) (agreed)

background
combine proofs (fat, focus)
- syntactic combine
- proof ordering
evaluation
- use TSTP proof and find interesting results
- show several interesting results and statistics
user interaction (thin)
- browse proofs: local view and global view
- search proofs:

paper outline (suggested by Paulo)

We already have TPTP
PML is a new way of publishing TPTP proofs based on WEB technologies: OWL, PML, URIs
New proof graph
- Truly distributed
- Now we can combine proof fragments
- We have tools to visualize these combined proofs
Open issues
- How to best combine fragments
- How to compare two proofs - one is better than the other?
  - number of InferenceSteps
  - maximal depth
  - average depth
  - number of context NodeSets
  - geometric considerations in proof complexity (for deduction system)
- How to best present combined proofs

proof combination (compare the original and optimal)
- # of nodes
- # of leaf nodes
- # of depth
local browser
proof search

next meeting on 10-21
todo: Cynthia - can you find a selection of proofs for PUZ001+1 than leads to a combination that is obviously better than any of the originals?