Abstract

In this work, formulas are inclusions \ and non-inclusions \ between Boolean terms \ and \. We present a set of rules through which one can transform a term t in a diagram \ and, consequently, each inclusion \ ) in an inclusion \ ) between diagrams. Also, by applying the rules just to the diagrams we are able to solve the problem of verifying if a formula \ is consequence of a, possibly empty, set \ of formulas taken as hypotheses. Our system has a diagrammatic language based on Venn diagrams that are read as sets, and not as statements about sets, as usual. We present syntax and semantics of the diagrammatic language, define a set of rules for proving consequence, and prove that our set of rules is strongly sound and complete in the following sense: given a set \ of formulas, \ is a consequence of \ iff there is a proof of this fact that is based only on the rules of the system and involves only diagrams associated to \ and to the members of \.