Matching logic (a first-order logic variant) has been proposed as a unifying logic for specifying and reasoning about (structure of) programs. Since the logic itself is relatively young, there is still much we do not know, even if we consider basic matching logic without extensions (like Matching mu-Logic). The goal of this thesis is to try to advance our knowledge about matching logic and especially its proof systems. Possible topics include proving completeness and/or related results, giving new matching logic extensions, finding connections to other logics or formalizing some of the existing proofs in the Coq proof assistant.