Many algorithms for automated reasoning use first-order predicate calculus with equality or different flavors of category theory. BTS takes a different path. It employs a graphical and algebraic formalism grounded in graph rewriting and category theory that can also be interpreted geometrically in some cases. At the heart of this approach lie monoidal categories, which form the cornerstone of categorical algebra, connecting algebra, topology, and computer science. Bigraphical Reactive Systems bring this formal framework into practical application.