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

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