Extended Horn sets in propositional logic

DOI10.1145/102782.102789MaRDI QIDQ4302833zbMATH OpenOpenAlexFDO

Authors

Publication date 29 September 1994

Published in Journal of the ACM (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/102782.102789

Mathematics Subject Classification ID

Classical propositional logic (03B05) Logic programming (68N17) Logic in artificial intelligence (68T27)

Recommendations

• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• Recognition of simple enlarged Horn formulas and simple extended Horn formulas
• On finding solutions for extended Horn formulas
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• The horn basis of a set of clauses

Cited in

(43)

• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• Logic applied to integer programming and integer programming applied to logic
• Detecting embedded Horn structure in propositional logic
• New methods for computing inferences in first order logic
• Computing definite logic programs by partial instantiation
• A rounding algorithm for integer programs
• Recognition of q-Horn formulae in linear time
• Hierarchies of polynomially solvable satisfiability problems
• Pseudo-models and propositional Horn inference
• On exact selection of minimally unsatisfiable subformulae
• Solving the resolution-free SAT problem by submodel propagation in linear time
• Recognizing renamable generalized propositional Horn formulas is NP- complete
• Balanced \(0,\pm 1\) matrices. I: Decomposition
• A short note on some tractable cases of the satisfiability problem.
• A perspective on certain polynomial-time solvable classes of satisfiability
• Recognition of simple enlarged Horn formulas and simple extended Horn formulas
• The arborescence-realization problem
• A new algorithm for the propositional satisfiability problem
• Maximum renamable Horn sub-CNFs
• Mixed logical-linear programming
• Recognition of tractable satisfiability problems through balanced polynomial representations
• On some tractable classes in deduction and abduction
• The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas
• Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing
• Domain permutation reduction for constraint satisfaction problems
• Balanced matrices
• A sharp threshold for the renameable-Horn and the \(q\)-Horn properties
• Typical case complexity of satisfiability algorithms and the threshold phenomenon
• Properties of SLUR Formulae
• scientific article; zbMATH DE number 4037814 (Why is no real title available?)
• The horn basis of a set of clauses
• The phase transition in random horn satisfiability and its algorithmic implications
• Incremental methods for optimizing partial instantiation
• About some UP-based polynomial fragments of SAT
• Mathematical Foundations of Computer Science 2005
• On the Boolean connectivity problem for Horn relations
• A logic-based approach to polymer sequence analysis
• Computing minimal models by partial instantiation
• On finding solutions for extended Horn formulas
• Unit refutability of Horn constraint systems -- certification and parallel complexity
• Ideal clutters
• Solving peptide sequencing as satisfiability
• Translating propositional extended conjunctions of Horn clauses into Boolean circuits

Describes a project that uses

Uses Software

• Ltur

This page was built for publication: Extended Horn sets in propositional logic

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