Polynomial-time inference of all valid implications for Horn and related formulae

DOI10.1007/BF01531068zbMath0878.68105MaRDI QIDQ1356205

Endre Boros, Yves Cramer, Peter L. Hammer

Publication date: 14 December 1997

Published in: Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

zbMATH Keywords

inference problemHorn formulae

Mathematics Subject Classification ID

Related Items (37)

Recognition of \(q\)-Horn formulae in linear time ⋮ On perfect \(0,\pm 1\) matrices ⋮ Known and new classes of generalized Horn formulae with polynomial recognition and SAT testing ⋮ On the size of maximum renamable Horn sub-CNF ⋮ On propositional definability ⋮ Variable and term removal from Boolean formulae ⋮ PALO: a probabilistic hill-climbing algorithm ⋮ Hierarchies of polynomially solvable satisfiability problems ⋮ Unique key Horn functions ⋮ A CNF Class Generalizing Exact Linear Formulas ⋮ Properties of quasi-Boolean function on quasi-Boolean algebra ⋮ Variations on extending partially defined Boolean functions with missing bits. ⋮ SAT backdoors: depth beats size ⋮ Lean clause-sets: Generalizations of minimally unsatisfiable clause-sets ⋮ Trichotomy for integer linear systems based on their sign patterns ⋮ Balanced matrices ⋮ Incremental polynomial time dualization of quadratic functions and a subclass of degree-\(k\) functions ⋮ Maximum renamable Horn sub-CNFs ⋮ On connected Boolean functions ⋮ A logic-based approach to polymer sequence analysis ⋮ A CNF Formula Hierarchy over the Hypercube ⋮ Solving peptide sequencing as satisfiability ⋮ Bounds on the size of PC and URC formulas ⋮ On some tractable classes in deduction and abduction ⋮ Autark assignments of Horn CNFs ⋮ Horn functions and their DNFs ⋮ Consensus algorithms for the generation of all maximal bicliques ⋮ On exact selection of minimally unsatisfiable subformulae ⋮ Satisfiability of mixed Horn formulas ⋮ Strong Backdoors for Default Logic ⋮ Investigations on autark assignments ⋮ Default reasoning from conditional knowledge bases: Complexity and tractable cases ⋮ The Horn renamability, q-Horn and SLUR threshold for random \(k\)-CNF formulas ⋮ A linear time algorithm for unique Horn satisfiability ⋮ The complexity of theory revision ⋮ On functional dependencies in \(q\)-Horn theories ⋮ Backdoors to q-Horn

Uses Software

• Ltur

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• LTUR: A simplified linear-time unit resolution algorithm for Horn formulae and computer implementation
• A cascade algorithm for the logical closure of a set of binary relations
• Complete problems for deterministic polynomial time
• A linear-time algorithm for testing the truth of certain quantified Boolean formulas
• Question-asking strategies for Horn clause systems
• A Way to Simplify Truth Functions
• Linear-time algorithms for testing the satisfiability of propositional horn formulae
• A linear expected-time algorithm for deriving all logical conclusions implied by a set of boolean inequalities
• Unification as a complexity measure for logic programming
• The Complexity of Enumeration and Reliability Problems
• Recognizing disguised NR(1) instances of the satisfiability problem
• Renaming a Set of Clauses as a Horn Set
• The complexity of satisfiability problems
• A Machine-Oriented Logic Based on the Resolution Principle
• On Cores and Prime Implicants of Truth Functions
• The complexity of theorem-proving procedures

This page was built for publication: Polynomial-time inference of all valid implications for Horn and related formulae