On a graph calculus for algebras of relations

Abstract

We present a sound and complete logical system for deriving 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 complete one to cope with proofs from hypotheses. This leads to a system dealing with complementation. Other approaches using pictures for relations use as bases the theory of allegories or rewriting systems. Our formalism is more widely applicable and provides a common denominator of these approaches. © 2008 Springer-Verlag Berlin Heidelberg.