Using relation-algebraic means and tool support for investigating and computing bipartitions

Using Dedekind categories as an algebraic structure for (binary) set-theoretic relations without complements, we present purely algebraic definitions of “to be bipartite” and “to possess no odd cycles” and prove that both notions coincide in case that the reflexive-transitive closure of the relation in question is symmetric. This generalises D. Kőnig's well-known theorem from undirected graphs to abstract relations and, hence, to models such as L-relations that are different from set-theoretic relations. One direction of this generalisation holds for general relations. The other direction requires the symmetry of the reflexive-transitive closure as premise and is shown by specifying a bipartition for the given relation in form of a pair of disjoint relational vectors. For set-theoretic relations this immediately leads to a relational program for computing a bipartition. We also investigate the structure of a certain set of bipartitions that is generated by a given bipartition, explore the set of all bipartitions of a bipartite relation with respect to minimality and maximality of elements in view of the component-wise inclusion, show a relationship between bipartitions and bichromatic partitions and also discuss how the algebraic proofs can be mechanised using theorem proving tools.