Basic ATP System Requirements

Soundness and Completeness

• Soundness is required
  • Extensive testing
  • Verifiable (and verified) proof/model output
• Completeness is not required
  • Theoretically possible
  • Practically impossible
  • Might be undesirable

Deployment

• Download, unpack, build, install
• Commonly available compilers and build tools
  • Not at the bleeding edge
• Configuration and makefiles
• Encapsulated and movable installation

Deploy and Use

• Novice and advanced options
• TPTP compliance: input, SZS status, proofs/models
• Meaningful error messages
• React to signals appropriately
• Leave no dingo poop processes or files
• Liberal licensing