- 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

- The ATP requirements, which determine

- The syntax of the representation, which determine

- The representation requirements, which determine

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

- Many (syntactically different) representations, allowing

- The syntax of the representation can determine
- A model of the mathematical notion, which can guide
- The ATP system

- A model of the mathematical notion, which can guide
- An external representation of the mathematical notion might guide
- The ATP system