Conclusion

Establishing Standards

• The standards are in use
  • Deduction systems, e.g., E, Faust, YuLM ...
  • Deduction management systems, e.g., MPTP, MathWeb-SB ...
  • TPTP v3.0.0 & TSTP
• Actions Speak Louder than Committees
  • Highly pragmatic standards
  • Careful thought, community input, decisions
  • Application and feedback
• Future Work
  • Standards for models
  • Language for tableaux

Using Tools

• The tools are in use
  • Isabelle
  • NASA
  • MathWeb-SB
  • ARTists
  • TPTP users
• Future Work
  • Distribution packaging
  • The formulator