Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic

DOI10.1016/0020-0190(86)90136-5MaRDI QIDQ1819946zbMATH OpenOpenAlexFDO

Authors Susumu Yamasaki, Shuji Doshita

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

zbMATH Keywords

computational complexitylinear layered resolution deductionnon-Horn sentencesNP-completenesspropositional Horn-clause logicsatisfiability problem

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Analysis of algorithms and problem complexity (68Q25)

Review text

The computational complexity of the propositional Horn-clause logic is significant, since its satisfiability is decidable in polynomial time, although the satisfiability problem of the propositional logic is NP- complete. From the standpoint of NP-completeness, there have been many attempts to extend as much as possible the class of propositional formulae for which the satisfiability problem is in P. This paper is thought of as such an attempt. We propose a class of non-Horn sentences, for which the satisfiability problem is in P. To detect the satisfiability for such a class, we treat an extended version of linear layered resolution deduction based on input deductions, which is formed by repetitions of input deductions with derived unit clauses to be memorized.

Recommendations

• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic
• scientific article; zbMATH DE number 702472
• The computational complexity of the satisfiability of modal Horn clauses for modal propositional logics
• An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences
• scientific article; zbMATH DE number 1470716

Cites work

• Complete problems for deterministic polynomial time
• Horn clause computability
• scientific article; zbMATH DE number 3466489 (Why is no real title available?)
• scientific article; zbMATH DE number 3566230 (Why is no real title available?)
• scientific article; zbMATH DE number 3571502 (Why is no real title available?)
• scientific article; zbMATH DE number 3639144 (Why is no real title available?)
• scientific article; zbMATH DE number 3449757 (Why is no real title available?)
• On the complexity of regular resolution and the Davis-Putnam procedure
• Resolution Strategies as Decision Procedures
• The Specialization of Programs by Theorem Proving
• Unit Refutations and Horn Sets

Cited in

(1)

• The satisfiabilty problem for a class consisting of horn sentences and some non-horn sentences in proportional logic

This page was built for publication: Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic

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