Conclusion

• Fulfilled the main aims and motivations
  • Evaluated the relative abilities of cuurrent ATP systems
  • Stimulated development of and interest in ATP systems

• Development efforts have received public recognition
  • Provided exposure for system builders ... both within and beyond the community
  • Provided an overview of the implementation state of running, fully automatic, first order ATP systems
  • Trophies will be presented at the banquet

  

• Next year and Beyond
  • More focus on full FOF proofs and models
  • New THF (typed higher-order form) demonstration division
    (Please check out the syntax following links from the TPTP site.)
  • Cancellation of divisions with no new problems or entrants
  • Potentially some serious $ prizes
  • Your Prover (You)

  • FLoCC - Federated Logic Conference Competitions

• The MPTP $100 Challenges