A note on proofs with graphs

AbstractCurtis and Lowe (S. Curtis, G. Lowe, Proofs with graphs, Sci. Comput. Program. 26 (1996) 197–216) presented a graphical calculus to prove inclusions between relations, leaving completeness of the system as an open question. Here we recast their system, excluding complementation and union, by presenting a low complexity decision algorithm to decide its valid inclusions. Completeness follows as a corollary