Binary resolution over Boolean lattices

We propose a binary resolution system over Boolean lattices. We shall assume that truth values form a complete Boolean lattice L where its supremum operator is infinitely distributive over the infimum one. Binary L-resolution will operate on graded clauses. A graded clause is a pair of the form (l1∨⋯∨ln,c) where li are literals and c is a truth degree in L. The refutational soundness and completeness of the proposed resolution proof method will be proved.