The Starting Point

Three Theorems

• Veroff used proof sketches to find proofs for ...

  P(i(i(x,y),j(x,y)))            %T1
  P(j(i(x,y),i(j(y,z),j(x,z))))  %T2
  P(j(i(y,z),i(j(x,y),j(x,z))))  %T3

• Search for short proofs of T1 and (T2 & T3)

Techniques

• Otter for proving
• Mace4 for model finding
• Ancestor subsumption to retain short derivations
• Demodulation to block use of formulae
• Resonators and cramming to guide proofs