title: Kowalski graph theorem proving
body: <p>I'm trying to use the Kowalski graph algorithm for resolution theorem
  proving. The description of the algorithm at
  <a href="http://www.doc.ic.ac.uk/~rak/" rel="nofollow noreferrer">http://www.doc.ic.ac.uk/~rak/</a> is silent on what to do about the large
  number of duplicate clauses it generates. I'm wondering if there's a
  well-known technique for dealing with them?</p>
  
  <p>In particular, you can't simply suppress the generation of duplicate
  clauses, because the links that come with them are relevant.</p>
  
  <p>It seems to me that it's probably necessary to track the set of all
  clauses generated thus far, and when a duplicate is generated, add the
  new links to the existing instance instead. This probably needs to be
  maintained even when a clause is nominally deleted, for when it is
  regenerated.</p>
  
  <p>Duplication probably needs to be defined in terms of textual
  representation, rather than object equality, because literals of
  different clauses are distinct objects even when they are identical.</p>
  
  <p>Can anyone confirm whether I'm on the right track here? Also, the only
  significant online reference I could find to this algorithm was the
  link above, does anyone know of any others, or any existing code
  implementing it?</p>