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

Analysis of algorithms and problem complexity (68Q25) Classical propositional logic (03B05)

Related Items

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