The following pages link to Unit Refutations and Horn Sets (Q4050192):
Displaying 42 items.
- On Davis-Putnam reductions for minimally unsatisfiable clause-sets (Q391124) (← links)
- Tradeoffs in the complexity of backdoors to satisfiability: dynamic sub-solvers and learning during search (Q457253) (← links)
- About some UP-based polynomial fragments of SAT (Q513329) (← links)
- Semantics and properties of existential quantifiers in deductive databases (Q685471) (← links)
- Algorithms for the maximum satisfiability problem (Q753502) (← links)
- Theorem-proving with resolution and superposition (Q757094) (← links)
- Trichotomy for integer linear systems based on their sign patterns (Q906434) (← links)
- Declarative modeling of the operational behavior of logic languages (Q913530) (← links)
- On solving the equality problem in theories defined by Horn clauses (Q1085152) (← links)
- Why Horn formulas matter in computer science: initial structures and generic examples (Q1089797) (← links)
- A fixpoint semantics of Horn sentences based on substitution sets (Q1100934) (← links)
- Optimizing propositional calculus formulas with regard to questions of deducibility (Q1117918) (← links)
- On renaming a set of clauses as a Horn set (Q1120278) (← links)
- Theorem proving with abstraction (Q1149799) (← links)
- A simplified problem reduction format (Q1170894) (← links)
- Complete problems for deterministic polynomial time (Q1235982) (← links)
- Automatic theorem proving in set theory (Q1245007) (← links)
- On renamable Horn and generalized Horn functions (Q1356207) (← links)
- Renaming a set of non-Horn clauses (Q1587332) (← links)
- Autark assignments of Horn CNFs (Q1742887) (← links)
- Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic (Q1819946) (← links)
- Horn equational theories and paramodulation (Q1824409) (← links)
- Efficient algorithms for qualitative reasoning about time (Q1855212) (← links)
- On computability by logic programs (Q1924787) (← links)
- On \(k\)-positive satisfiability problem (Q1964360) (← links)
- On some tractable classes in deduction and abduction (Q1978251) (← links)
- Branching interval algebra: an almost complete picture (Q2051838) (← links)
- Generalising unit-refutation completeness and SLUR via nested input resolution (Q2352484) (← links)
- Incremental qualitative temporal reasoning: Algorithms for the point algebra and the ORD-Horn class (Q2457656) (← links)
- Satisfiability with index dependency (Q2637283) (← links)
- Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems (Q2641226) (← links)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer (Q2818017) (← links)
- Efficient Reasoning for Inconsistent Horn Formulae (Q2835881) (← links)
- Generalising and Unifying SLUR and Unit-Refutation Completeness (Q2927648) (← links)
- Generalized Conflict-Clause Strengthening for Satisfiability Solvers (Q3007694) (← links)
- Strategies of the search for derivation of statements with restricted quantifiers (Q3675553) (← links)
- OnP-subset structures (Q3789542) (← links)
- Deduction-seeking procedures and transitive relations (Q3793763) (← links)
- Automatic theorem proving. II (Q3793764) (← links)
- The phase transition in random horn satisfiability and its algorithmic implications (Q4543632) (← links)
- A maximal-literal unit strategy for horn clauses (Q5881264) (← links)
- (Q6060092) (← links)
