Overview

ATP Proofs

• Proofs are DAGs, typically with a false root
• Written in the TPTP language
• Rendered with IDV

Combining Proof DAGs

• Repeatedly ...
  • Select replaced node in target proof
  • Find equivalent replacing node in contributing proof
  • Replace sub-DAG in target proof to form combined proof

• Requires an equivalence relation between nodes
• Might require same problem, or same background theory