Unit Refutations and Horn Sets

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
On some tractable classes in deduction and abduction
A maximal-literal unit strategy for horn clauses
Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
Optimizing propositional calculus formulas with regard to questions of deducibility
Autark assignments of Horn CNFs
On \(k\)-positive satisfiability problem
Automatic theorem proving in set theory
Strategies of the search for derivation of statements with restricted quantifiers
Deduction-seeking procedures and transitive relations
scientific article; zbMATH DE number 7760475 (Why is no real title available?)
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
Trichotomy for integer linear systems based on their sign patterns
Branching interval algebra: an almost complete picture
The phase transition in random horn satisfiability and its algorithmic implications
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
On solving the equality problem in theories defined by Horn clauses
Automatic theorem proving. II

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)