Existing Solution Languages

Purpose

• Existing languages are problem languages
• Just a few solution languages

ATP Systems' Outputs

• Text based
• Inconsistent with input languages
• For example, PCL
  • Text based
  • DISCOUNT and E theorem provers
  • Postprocessors available

ND Proofs