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.03010OpenAlexW2005101116MaRDI QIDQ3677734

Susumu Yamasaki, Shuji Doshita

Publication date: 1983

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

Full work available at URL: https://doi.org/10.1016/s0019-9958(83)80027-8

zbMATH Keywords

resolution principleHorn clause

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15)

Related Items

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