 Then there are non-distributive logics, in which the inference from \((A\land(B\lor C))\) to \(((A\land B)\lor(A\land C))\) is rejected: such logics have been proposed as quantum logics. A natural deduction system for such a logic (based on the form of sequent natural deduction used in Lemmon (1965), though Fitch-style versions are also possible) is given in the textbook, Gibbins 1987.