Resolution remains hard under equivalence
From MaRDI portal
Publication:1961451
DOI10.1016/S0166-218X(99)00055-4zbMath0941.68125MaRDI QIDQ1961451
Theodor Lettmann, Hans Kleine Büning
Publication date: 17 January 2000
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
Cites Work
- The intractability of resolution
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Controlled integration of the cut rule into connection tableau calculi
- An Implementation of the Model Elimination Proof Procedure
- The Complexity of Propositional Proofs
- Unnamed Item
- Unnamed Item
- Unnamed Item