# IW Meeting 2008-10-16

### From Inference Web

## Contents |

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

## Paper for AI communication

**paper call**

- http://www.csc.liv.ac.uk/~konev/AICom/
- Special Issue on Practical Aspects of Automated Reasoning (PAAR)
- 20-30 pages
- Deadline: 22 December 2008

**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

## demo for iswc

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

- local browser
- proof search

## notes

- 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?