Conclusion

The Maths is Important

• The mathematical notion determines
  • The representation requirements, which determine
    • The syntax of the representation, which determine
      • The ATP requirements, which determine
        • The choice of ATP system

It's One-to-Many

• One mathematical notion can have
  • Many (syntactically different) representations, allowing
    • A choice of ATP systems

The Maths can Help

• The syntax of the representation can determine
  • A model of the mathematical notion, which can guide
    • The ATP system
• An external representation of the mathematical notion might guide
  • The ATP system
  even better