Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
From MaRDI portal
Publication:1819946
DOI10.1016/0020-0190(86)90136-5zbMath0614.68063OpenAlexW1986931182MaRDI QIDQ1819946
Shuji Doshita, Susumu Yamasaki
Publication date: 1986
Published in: Information Processing Letters (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0020-0190(86)90136-5
computational complexityNP-completenesssatisfiability problemlinear layered resolution deductionnon-Horn sentencespropositional Horn-clause logic
Analysis of algorithms and problem complexity (68Q25) General topics in the theory of software (68N01)
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Complete problems for deterministic polynomial time
- On the complexity of regular resolution and the Davis-Putnam procedure
- Unit Refutations and Horn Sets
- Resolution Strategies as Decision Procedures
- Horn clause computability
- The Specialization of Programs by Theorem Proving