Unit Refutations and Horn Sets

DOI10.1145/321850.321857zbMath0296.68093WikidataQ114255234 ScholiaQ114255234MaRDI QIDQ4050192

Larry Wos, Lawrence J. Henschen

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

The phase transition in random horn satisfiability and its algorithmic implications, Semantics and properties of existential quantifiers in deductive databases, Algorithms for the maximum satisfiability problem, Theorem-proving with resolution and superposition, Declarative modeling of the operational behavior of logic languages, On solving the equality problem in theories defined by Horn clauses, Why Horn formulas matter in computer science: initial structures and generic examples, A fixpoint semantics of Horn sentences based on substitution sets, Optimizing propositional calculus formulas with regard to questions of deducibility, On renaming a set of clauses as a Horn set, Theorem proving with abstraction, A simplified problem reduction format, Complete problems for deterministic polynomial time, Automatic theorem proving in set theory, On renamable Horn and generalized Horn functions, Renaming a set of non-Horn clauses, Resolution deduction to detect satisfiability for another class including non-Horn sentences in propositional logic, Horn equational theories and paramodulation, Efficient algorithms for qualitative reasoning about time, On computability by logic programs, On \(k\)-positive satisfiability problem, On some tractable classes in deduction and abduction, Incremental qualitative temporal reasoning: Algorithms for the point algebra and the ORD-Horn class, Deadlocks and traps in Petri nets as Horn-satisfiability solutions and some related polynomially solvable problems, Strategies of the search for derivation of statements with restricted quantifiers, OnP-subset structures, Deduction-seeking procedures and transitive relations, Automatic theorem proving. II