A graph calculus for proving intuitionistic relation algebraic equations

Abstract

In this work, we present a diagrammatic system in which diagrams based on graphs represent binary relations and reasoning on binary relations is performed by transformations on diagrams. We proved that if a diagram D1 can be transformed into a diagram D2 using the rules of our system, under a set ∑ of hypotheses, then it is intuitionistically true that the relation defined by diagram D1 is a sub-relation of the one defined by diagram D2, under the hypotheses in ∑. © 2012 Springer-Verlag.