Unit Refutations and Horn Sets
From MaRDI portal
Publication:4050192
DOI10.1145/321850.321857zbMATH Open0296.68093OpenAlexW1998113645WikidataQ114255234 ScholiaQ114255234MaRDI QIDQ4050192FDOQ4050192
Authors: Lawrence 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
Cited In (41)
- Theorem proving with abstraction
- Semantics and properties of existential quantifiers in deductive databases
- On renaming a set of clauses as a Horn set
- Generalized conflict-clause strengthening for satisfiability solvers
- On computability by logic programs
- On renamable Horn and generalized Horn functions
- Horn equational theories and paramodulation
- A maximal-literal unit strategy for horn clauses
- On some tractable classes in deduction and abduction
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Autark assignments of Horn CNFs
- Optimizing propositional calculus formulas with regard to questions of deducibility
- Strategies of the search for derivation of statements with restricted quantifiers
- On \(k\)-positive satisfiability problem
- Automatic theorem proving in set theory
- Title not available (Why is that?)
- Deduction-seeking procedures and transitive relations
- Satisfiability with index dependency
- Generalising and unifying SLUR and unit-refutation completeness
- Renaming a set of non-Horn clauses
- Theorem-proving with resolution and superposition
- Why Horn formulas matter in computer science: initial structures and generic examples
- Complete problems for deterministic polynomial time
- Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search
- Generalising unit-refutation completeness and SLUR via nested input resolution
- Declarative modeling of the operational behavior of logic languages
- Incremental qualitative temporal reasoning: Algorithms for the point algebra and the ORD-Horn class
- The phase transition in random horn satisfiability and its algorithmic implications
- Branching interval algebra: an almost complete picture
- Trichotomy for integer linear systems based on their sign patterns
- A simplified problem reduction format
- Efficient algorithms for qualitative reasoning about time
- Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems
- A fixpoint semantics of Horn sentences based on substitution sets
- Efficient reasoning for inconsistent Horn formulae
- OnP-subset structures
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic
- About some UP-based polynomial fragments of SAT
- Algorithms for the maximum satisfiability problem
- Automatic theorem proving. II
- On solving the equality problem in theories defined by Horn clauses
This page was built for publication: Unit Refutations and Horn Sets
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4050192)