A synthesis of the resolution method and the inverse method

It is introduced a compact coding of (finite sets of) propositional formulas by means of plane configurations called diagrams. A special kind of diagrams (called closed ones) is defined by some pure combinatorial properties. It is proved that a formula is a tautology iff its diagram is closed. An inductive procedure of generation of all closed diagrams is described. This procedure combines the ideas of the resolution method [1] and the inverse method [2]. Some isomorphism between the mentioned methods is stated.