On a Graph Calculus for Algebras of Relations?

Abstract. We present a sound and complete logical system for deriv-ing inclusions between graphs from inclusions between graphs, taken as hypotheses. Graphs provide a natural tool for expressing relations and reasoning about them. Here we extend this system to a sound and com-plete one to cope with proofs from hypotheses. This leads to a system dealing with complementation. Other approaches using pictures for re-lations use as bases the theory of allegories or rewriting systems. Our formalism is more widely applicable and provides a common denomina-tor of these approaches. Key words: Relational language, reasoning from hypotheses, graph cal-culus, completeness, complementation