This chapter discusses a top-down approach to modelling soccer knowledge, as it can be found in soccer theory books. The goal is to model soccer strategies and tactics in a way that they are usable for multiple robotic soccer leagues in the RoboCup. We investigate if and how soccer theory can be formalized such that specification and execution are possible. The advantage is clear: theory abstracts from hardware and from specific situations in different leagues. We introduce basic primitives compliant with the terminology known in soccer theory, discuss an example on an abstract level and formalize it. The formalization of soccer presented here is appealing. It goes beyond the behaviour specification of soccer playing robots. For sports science a unified formal soccer theory might help to better understand and to formulate basic concepts in soccer. The possibility of the formalization to develop computer programs, which allow to simulate and to reason about soccer moves, might also take sports science a step further.