IW Meeting 2008-10-16

From Inference Web

Jump to: navigation, search


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 for AI communication

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

demo for iswc

  • 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?
Personal tools