A little-known fact is that this family of equivalent problems has a
representative in proof theory, a fact which has led researchers in logic to
independently rediscover equivalent versions of Kotzig's theorem. This
connection between the theory of proof net correctness in linear
logic [1]} and perfect matchings was first noticed by
Retoré [2]}, but remained unexploited for a long time. We
applied it in a previous paper [3]} in order to make
progress on open problems concerning proof nets. Conversely, here we demonstrate
some benefits of this bridge between logic and graphs for pure graph theory.
Some of the results we present here were directly motivated by logical
applications and are used either in [3]}, in its upcoming
journal version, or in our more recent work [5]}.
