Certain distributivity results for Lukasiewicz’s infinite-valued logic Lℵ0 are proved axiomatically (for the first time) with the help of the automated reasoning program Otter [16]. In addition, non -distributivity results are established for a wide variety of positive substructural logics by the use of logical matrices discovered with the automated model findingprograms Mace [15] and MaGIC [25].

This paper offers a particular intuitionistic negation completion of Urquhart's system C resulting in a super-intuitionistic contractionless propositional logic equivalent to Dummett's LC without contraction.