# IW Meeting 2009-03-05

### From Inference Web

2009-03-05

## agenda

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

## notes

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. Issues: 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

## todos

- 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