IW Meeting 2009-05-28

From Inference Web

Jump to: navigation, search
  • 2009-05-28



  • 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


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



  • 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
Facts about IW Meeting 2009-05-28RDF feed
Date28 May 2009  +
Personal tools