IW Meeting 2009-03-24

From Inference Web

Jump to: navigation, search
  • time: Tuesday morning
  • time: Wednesday noon-afternoon

Contents

agenda

IW Meeting 2009-03-19

  • review the general work framework TPTP-IW
  • quality measures
  • proof generation
    • mizar proof (a set of proofs for a set of theorem)
    • atp proof ( a set of proofs for one theorem)
  • two combine proof algorithm
  • evaluation strategy
  • paulo's example (low priority)

notes

Mar 24-25, 2009

translation

to generate PML proofs from TPTP. Right now we have two categories of combineable TPTP proofs.

  • atp proofs ( for each TPTP problem, we can combine the corresponding set of proofs)
    • we currently have a couple of thousands of problems
    • cynthia has translated almost all proofs to PML
  • mizar proof (a set of proofs for a set of theorem)
    • xboole proofs, translated
    • newton proofs, not translated ready yet.
    • need to translate more (thousands) Mizar proofs

mapping

(directional?) same as relation between conclusions (formula)

  • currently, Cynthia build a web service that re-generate PML proof once the ATP proofs have been re-generated
  • Cynthia has send Li a mapping file, for initial test
  • we will generate more (>1000) mapping files (from all TPTP problems) to get statistically interesting results


metrics

1. (total order) minimize total number of cnfs conclusion in proof 

    P1
A(fof)  B(fof)           
 \      /
  D(cnf)   C(fof)
     \    /
       E(cnf)

    P2
 X(cnf)  Y(cnf)           
     \    /
       E(cnf)

In the above example, proof P2 is better because it has less cnf formula

2. (partial order) a proof is better than another if its used axioms are subset of their other's 

  P3 concludes E using three axioms (A,B,C)
  P4 concludes E using two axioms (A,B)
  P5 concludes E using two axioms (A,D)

In the above example, P4 is better than P3. but there is no such partial order relation between p5 and p3

3. (total order) minimize the axioms used. we use the same examples

  • In the examples, P4 is better than P5 because is uses (A,D) 2 instead of (A,B,C) 3 axioms. so does P4.
  • intuition: the less axioms used, given all axioms are equality trustworthy but not fully trustworthy, the better we can trust them jointly.
  • another intuition: consider a truth value table for all the axioms, less number of axioms lead to more matching lines.
  • (total order) minimize the false rows in truth value table given all possible proofs

precondition

  • a proof should not show the same conclusion twice
  • we treat a proof as a DAG, no matter used how many time, an axioms is counted just once.
  • a proof typically only has one final conclusion

precondition for counting axiom

  • if i have a fof problem, I must see at least one fof leaves
    • language of the leaves must be the same as the language of the problem.
  • for FOF problem, I only count FOF axioms, so does CNF problem.

probabilistic interpretation

we consider a proof as a Bayes Network. a proof in form of (conclusion, antecedents) can be mapped as the following:

  • node for formulae
  • arc for dependency

step1: consider there is just one proof

  • if we know the proof uses a set of antecedent: p(proof) can be interpreted as p(antecedents); 
 p(E)= p(E|A,B,C) p(A,B,C)
  • if we assume all axioms are independent. 
 p(E)=  p(E|A) p(E|B) p(E|C) p(A) p(B) p(C)

TODO


step2: consider there are many proofs. can we compute some more?

Jie's ciations

Below are the papers I mentioned over lunch the other day on selecting fragments of a logic theory. Both are handling with making choices between multiple possible candidates.

Z. Huang, F. van Harmelen, and A. ten Teije. Reasoning with inconsistent ontologies. In Proc. of IJCAI’05, pages 254–259. 2005 http://www.cs.vu.nl/~annette/pdf/IJCAI05.pdf

Franz Baader and Boontawee Suntisrivaraporn. Debugging SNOMED CT using axiom pinpointing in the description logic EL+. In Proc. of KR-MED’08, volume 410 of CEUR-WS, 2008. http://lat.inf.tu-dresden.de/research/papers/2008/BaaSun-KRMED-08.pdf


action items

  • mizar proof, clean up translation problems in newton (cynthia, geoff)
  • generate one conclusion mapping file (pairs of conclusions which are the same) for each problem (cynthia)
  • realize the metrics in combine algorithm (li)
Retrieved from "http://inference-web.org/wiki/IW_Meeting_2009-03-24"
Personal tools
Navigation