https://doi.org/10.3888/tmj.22-4 A method of generating minimally unsatisfiable conjunctive normal forms is introduced. A conjunctive normal form (CNF) is minimally unsatisfiable if it is unsatisfiable and such that removing any one of its clauses results in a satisfiable CNF. Introduction Ivor Spence [1] introduced a method for producing small unsatisfiable formulas of propositional logic that were … Continue reading Generating Minimally Unsatisfiable Conjunctive Normal Forms