scientific article; zbMATH DE number 1342212

zbMath0934.03015MaRDI QIDQ4263797

Hans Kleine Büning

Publication date: 22 September 1999

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

conjunctive normal formlength of proofsminimal unsatisfiable formulasupper bounds for minimal resolution refutations of propositional formulas

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Complexity of proofs (03F20)

Related Items (8)

Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Homomorphisms of conjunctive normal forms. ⋮ Minimal unsatisfiable formulas with bounded clause-variable difference are fixed-parameter tractable ⋮ An upper bound for the circuit complexity of existentially quantified Boolean formulas ⋮ The Lovász Local Lemma and Satisfiability ⋮ On subclasses of minimal unsatisfiable formulas ⋮ Investigations on autark assignments ⋮ Polynomial-time recognition of minimal unsatisfiable formulas with fixed clause-variable difference.

This page was built for publication: