Resolution remains hard under equivalence

DOI10.1016/S0166-218X(99)00055-4MaRDI QIDQ1961451zbMATH OpenFDO

Authors Hans Kleine Büning, Theodor Lettmann

Publication date 17 January 2000

Published in Discrete Applied Mathematics (Search for Journal in Brave)

zbMATH Keywords

proof systems

Mathematics Subject Classification ID

Recommendations

• Automating resolution is NP-hard
• The intractability of resolution
• Optimizing propositional calculus formulas with regard to questions of deducibility
• Finding the hardest formulas for resolution
• On resolution with short clauses

Cites work

• scientific article; zbMATH DE number 3583767 (Why is no real title available?)
• scientific article; zbMATH DE number 1037485 (Why is no real title available?)
• scientific article; zbMATH DE number 3415409 (Why is no real title available?)
• An Implementation of the Model Elimination Proof Procedure
• Controlled integration of the cut rule into connection tableau calculi
• Optimizing propositional calculus formulas with regard to questions of deducibility
• The Complexity of Propositional Proofs
• The intractability of resolution

Cited in

(3)

• NP-logic systems and model-equivalence reductions
• scientific article; zbMATH DE number 4085615 (Why is no real title available?)
• Finding the hardest formulas for resolution

This page was built for publication: Resolution remains hard under equivalence

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1961451)