Extending SLD resolution to equational horn clauses using E-unification
- 1 January 1989
- journal article
- Published by Elsevier in The Journal of Logic Programming
- Vol. 6 (1-2) , 3-43
- https://doi.org/10.1016/0743-1066(89)90028-9
Abstract
No abstract availableKeywords
This publication has 25 references indexed in Scilit:
- Fast algorithms for testing unsatisfiability of ground horn clauses with equationsJournal of Symbolic Computation, 1987
- Linear-time algorithms for testing the satisfiability of propositional horn formulaeThe Journal of Logic Programming, 1984
- A theory of complete logic programs with equalityThe Journal of Logic Programming, 1984
- Oriented equational clauses as a programming languageThe Journal of Logic Programming, 1984
- Contributions to the Theory of Logic ProgrammingJournal of the ACM, 1982
- Programming with EquationsACM Transactions on Programming Languages and Systems, 1982
- Variations on the Common Subexpression ProblemJournal of the ACM, 1980
- Reasoning About Recursively Defined Data StructuresJournal of the ACM, 1980
- Fast Decision Procedures Based on Congruence ClosureJournal of the ACM, 1980
- Logic programming and compiler writingSoftware: Practice and Experience, 1980