Logical completeness for string diagrams

String diagrams can be used as a compositional syntax fordifferent kinds of computational structures. This thesisviews string diagrams through a logical/universal algebraicperspective – diagrams represent formulas, allowingthe use of diagrammatic reasoning for proofs. Thecategory theoretic backdrop of this playground is givenby the concept of Cartesian bicategory – a categorical algebraof relations – that we consider as a relational theorythrough the lens of functorial semantics. Given a Cartesianbicategory, functorial semantics provides us with anappropriate notion of model as a structure-preserving functorto the category of sets and relations.Functoriality implies that diagrammatic reasoning is sound.The central question this approach raises and that we shallsettle is the question of completeness in the logical sense:does every property that is shared by all models have adiagrammatic proof?The main result of the thesis is a positive answer to theabove question. To show this, we give a combinatorialcharacterisation of Cartesian bicategories in terms of hypergraphsequipped with interfaces, inspired by a seminalresult by Chandra and Merlin. This reduces the problemof logical completeness to a categorical lifting problemthat we solve using a transfinite construction and acompactness argument.