Unit Refutations and Horn Sets

DOI10.1145/321850.321857zbMath0296.68093OpenAlexW1998113645WikidataQ114255234 ScholiaQ114255234MaRDI QIDQ4050192

Lawrence J. Henschen, Larry Wos

Publication date: 1974

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

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

Mathematics Subject Classification ID

Related Items (42)

A maximal-literal unit strategy for horn clauses ⋮ On solving the equality problem in theories defined by Horn clauses ⋮ Why Horn formulas matter in computer science: initial structures and generic examples ⋮ The phase transition in random horn satisfiability and its algorithmic implications ⋮ Satisfiability with index dependency ⋮ A fixpoint semantics of Horn sentences based on substitution sets ⋮ On renamable Horn and generalized Horn functions ⋮ Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems ⋮ Generalising and Unifying SLUR and Unit-Refutation Completeness ⋮ Optimizing propositional calculus formulas with regard to questions of deducibility ⋮ On renaming a set of clauses as a Horn set ⋮ On computability by logic programs ⋮ On Davis-Putnam reductions for minimally unsatisfiable clause-sets ⋮ Theorem proving with abstraction ⋮ Trichotomy for integer linear systems based on their sign patterns ⋮ Declarative modeling of the operational behavior of logic languages ⋮ OnP-subset structures ⋮ Unnamed Item ⋮ Deduction-seeking procedures and transitive relations ⋮ Automatic theorem proving. II ⋮ Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search ⋮ On \(k\)-positive satisfiability problem ⋮ A simplified problem reduction format ⋮ Incremental qualitative temporal reasoning: Algorithms for the point algebra and the ORD-Horn class ⋮ On some tractable classes in deduction and abduction ⋮ Generalized Conflict-Clause Strengthening for Satisfiability Solvers ⋮ Autark assignments of Horn CNFs ⋮ About some UP-based polynomial fragments of SAT ⋮ Semantics and properties of existential quantifiers in deductive databases ⋮ Complete problems for deterministic polynomial time ⋮ Automatic theorem proving in set theory ⋮ Branching interval algebra: an almost complete picture ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ Algorithms for the maximum satisfiability problem ⋮ Theorem-proving with resolution and superposition ⋮ Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic ⋮ Horn equational theories and paramodulation ⋮ Efficient Reasoning for Inconsistent Horn Formulae ⋮ Renaming a set of non-Horn clauses ⋮ Strategies of the search for derivation of statements with restricted quantifiers ⋮ Efficient algorithms for qualitative reasoning about time ⋮ Generalising unit-refutation completeness and SLUR via nested input resolution

This page was built for publication: Unit Refutations and Horn Sets