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

DOI10.1016/S0019-9958(83)80027-8zbMath0564.03010MaRDI QIDQ3677734

Shuji Doshita, Susumu Yamasaki

Publication date: 1983

Published in: Information and Control (Search for Journal in Brave)

zbMATH Keywords

resolution principle; Horn clause

Mathematics Subject Classification ID

68Q25: Analysis of algorithms and problem complexity

03B25: Decidability of theories and sets of sentences

03B35: Mechanization of proofs and logical operations

03D15: Complexity of computation (including implicit computational complexity)

Related Items

On generalized Horn formulas and \(k\)-resolution, Algorithms for the maximum satisfiability problem, An \(O(n^ 2)\) algorithm for the satisfiability problem of a subset of propositional sentences in CNF that includes all Horn sentences, Polynomially solvable satisfiability problems, A hierarchy of tractable satisfiability problems, On renamable Horn and generalized Horn functions, On resolution with short clauses, Hierarchies of polynomially solvable satisfiability problems, Recognizing renamable generalized propositional Horn formulas is NP- complete, Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing, Satisfiability with index dependency