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

  

• Next year
  • New systems
    • Wgandalf (Tanel Tammet)
    • Equinox (Koen Claessen)
    • SomethingFromStanford (Selene Makarios)
    • YourProver (You)
  • FOF promoted to premier status
  • Problems with arithmetic, demonstration division
  • More TPTP conformance