Vampire Basics

Soundness and Completeness

• Soundness is required : Probably :-)
  • Extensive testing: No contradictions in TSTP
  • Proof/model output: Refutations and saturations (not verified?)
• Completeness is not required
  • Theoretically possible : Calculus is complete
  • Practically impossible : Implementation is not (of course)

Deployment

• Download, unpack, build, install : No download right now
• Commonly available compilers and build tools : C++
• Configuration and makefiles : No sources distributed
• Encapsulated and movable installation : Single binary - perfect

Deploy and Use

• Novice and advanced options : Auto-mode and a Zog of options
• TPTP compliance, input, SZS status, proofs/models : Excellent
• Meaningful error messages : Not evaluated
• React to signals appropriately : Yes
• Leave no dingo poop processes or files : None
• Liberal licensing : Non-standard, but liberal