Patrick's Proof Display

Tree Display

• Input proofs in TSTP format
• WWW GUI
• Alternate subtrees
• Lemma detection by bushiness
• Proof merging

Refutations and Proofs

• Refutations are proof by contradiction
• Proofs are in the Hilbert style
• Conversion is possible, with a few caveats
  • Syntactic conversion
  • Semantic conversion using refutation to guide proof