Extending SLD resolution to equational horn clauses using E-unification

DOI10.1016/0743-1066(89)90028-9zbMath0668.68111OpenAlexW2038232291WikidataQ127613923 ScholiaQ127613923MaRDI QIDQ3821637

Stan Raatz, Jean H. Gallier

Publication date: 1989

Published in: The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0743-1066(89)90028-9

zbMATH Keywords

completenessunificationfunctional programmingrefutationcongruence closureSLD resolutionequational Horn clausesequational logic programs

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items (9)

Default reasoning by deductive planning ⋮ Fast algorithms for testing unsatisfiability of ground Horn clauses with equations ⋮ Incremental constraint satisfaction for equational logic programming ⋮ Combination problems for commutative/monoidal theories or how algebra can help in equational unification ⋮ Conditional equational theories and complete sets of transformations ⋮ A new deductive approach to planning ⋮ A compositional semantic basis for the analysis of equational Horn programs ⋮ Complete sets of transformations for general E-unification ⋮ Horn equational theories and paramodulation

This page was built for publication: Extending SLD resolution to equational horn clauses using E-unification