Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
From MaRDI portal
Publication:1100933
DOI10.1016/S0747-7171(87)80067-6zbMath0641.68146OpenAlexW2033598071MaRDI QIDQ1100933
Publication date: 1987
Published in: Journal of Symbolic Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/s0747-7171(87)80067-6
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (2)
Conditional congruence closure over uninterpreted and interpreted symbols ⋮ Canonical Ground Horn Theories
Cites Work
- Unnamed Item
- Unnamed Item
- Linear-time algorithms for testing the satisfiability of propositional horn formulae
- Extending SLD resolution to equational horn clauses using E-unification
- Fast Decision Procedures Based on Congruence Closure
- Variations on the Common Subexpression Problem
- Reasoning About Recursively Defined Data Structures
- Positive First-Order Logic Is NP-Complete
- Contributions to the Theory of Logic Programming
- Efficiency of a Good But Not Linear Set Union Algorithm
- The Semantics of Predicate Logic as a Programming Language
This page was built for publication: Fast algorithms for testing unsatisfiability of ground Horn clauses with equations
