# IW Meeting 2009-05-28

### From Inference Web

- 2009-05-28

## Contents |

## agenda

- progress on understanding the proof improvements / combination work (with background of thinking how this will help us write the evaluation section when we get to writing this up)
- high level complexity progress
- progress on representing the provenance challenge representation and question answering options. http://tw.rpi.edu/wiki/TetherlessPC3

## notes

complexity analysis linked justification (honglei)

- conclusion (closed a former loophole): counting solutions is #P complete
- proof (2SAT => AJ)
- proof (AJ => SAT)

- it is computationally impossible enumerate all solutions
- related work: AO* search 1970s (Nil Nilson) NP complete
- efficient algorithm - semi-optimal
- combine with several examples
- other greedy algorithm (future direction: how to deal with larger problems)
- Geoff: we do want to go for MUCH bigger sets of much bigger proofs with many more equal nodes, i.e., we need a heuristic approach of the ilk of the one Cynthia implemented.

proof combine (cynthia)

- combined proof in pml translated into tptp
- syntactically is correct, not yet loaded in tool

## discussion on Cynthia's counting function

cynthia's proposal

> To count the possible number of derivations of a proof boils done nodesets > and inference steps in the > proof. So if we can count the number of derivations of each nodeset and > inference step, then we know the > number for the proof. > > For an inference step, the total number of derivations depends on its > antecedents(nodesets)'s derivations. > So for a inference step IS, its number of derivation can be obtained by > multiply the derivation number of > all its antecedent: > IS(#d) = a1(#d) x a2(#d) x ... x an(#d) > > For a nodeset NS, its total number of derivations can be obtained from its > inference steps derivation > numbers: > NS(#d) = is1(#d) + is2(#d) + ... + isn(#d)

note: the above algorithm may work on tree but not necessarily on DAG

example2: honglei provided a counter example

- there should be 2 proofs
- but the function above counts 4 proofs: NS(T) = IS(e1) = NS(a) * NS(b)= ... = NS(c) * NS (c) =... = 2 * 2 =4

## todo

- honglei and Li work on the proof of "counting solutions is #P complete"
- cynthia and honglei and li review the formula on counting total solution
- compare li and cynthia's generated combined proofs
- connect PSL with TPTP combine