IW Meeting 2009-03-05

From Inference Web

Jump to: navigation, search



  • review IW Meeting 2009-02-26
  • backtrack provenance of combined proof
  • mizar translation
  • combine proof report
  • dump term equivalence relation


backtrack provenance of combined proof

  • change name (agreed)
  • drop max cardinality restriction
  • point to ordered list

isfromanswer (generated by Cynthia)

I'll bring up a picture first:

 s1     s2
 /       /
 ai1    ai2
 |        |
 A1    A2
 ^^     ^^
 |        |
 bi1   bi2
 |        |
 B1   B2
 ^^     ^^
 |        |
 ci1    ci2
 |        |
 C1    C2
 ^^     ^^
 |        |
 di1    di2
 |        |
 D1    D2

Let's say originally:
1. There are two proofs P1 and P2.
2. P1 has NodeSets A1, B1, C1 and D1 and inference steps ai1, bi1, ci1, di1.
3. P2 has NodeSets A2, B2, C2 and D2 and inference steps ai2, bi2, ci2, di2.
4. ai1, bi1 and ci1 all have isFromAnswer value of D1, which is the root.
5. ai2, bi2 and ci2 all have isFromAnswer value of D2, which is the root.
6. ai1 has source s1.
7. ai2 has source s2.

During the combining process, we find that C1 and C2 are equal and ci2 has
"better" measurement than ci1, therefore C1 and C2 can be combined. So
a inference step ci2' is created with:
1. B2 as its antecedent.
2. D1 (not D2) as its isFromAnswer.
Then ci2' is added to C1's isConsequentOf.

1. ci2 and ci2' are basically the same except the value of isFromAnswer,
  one is D2, and the other is D1.
2. For bi2 and ai2, their isFromAnswer is still D2 although they can be used to
  conclude both D2 and D1.
3. Source s2 is now used by both D2 and D1, but ai2 is not saying that because
  it only has one isFromAnswer which is D2.

What I would like is to relax the maxCard of isFromAnswer.
  • I am not sure we will have "isFromAnswer" in the combined proof
  • We already have it in the original proofs and we may need to leverage that (as opposed to combining them at the combined proof)
  • "it" I mean "isFromAnswer"
  • whatever is the solution, it also need to be good for abstracted proofs


  • Paulo - think about it - how to handle isaswerfrom in combined proofs (taking into consideration the use of hasOriginalProof)
  • geoff - keep on looking interesting point for funded project
Facts about IW Meeting 2009-03-05RDF feed
Date5 March 2009  +
Personal tools