On resolution with short clauses

DOI10.1007/BF02127749zbMath0892.03004MaRDI QIDQ1380411

Hans Kleine Büning, Michael Buro

Publication date: 11 May 1998

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

algorithmconjunctive normal form\(k\)-resolutionminimal proof lengths

Mathematics Subject Classification ID

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

Related Items (1)

Filter-based resolution principle for lattice-valued propositional logic LP\((X)\)

Cites Work

• Unnamed Item
• Unnamed Item
• On generalized Horn formulas and \(k\)-resolution
• The intractability of resolution
• Polynomially solvable satisfiability problems
• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• Linear-time algorithms for testing the satisfiability of propositional horn formulae

This page was built for publication: On resolution with short clauses