A note on semantics of logic programs with equality based on complete sets of E-unifiers

Anatoli Degtyarev, Andrei Voronkov

    Research output: Contribution to journalArticlepeer-review

    Abstract

    We discuss semantics of equational Horn-clause programs based on the notion of a complete set of E-unifiers. We prove incompleteness of SLDE†-resolution in the general case. SLDE†-resolution was introduced by Gallier and Raatz who proved its completeness for the case of well-behaved programs. We also define and compare several fixpoint semantics based on complete sets of E-unifiers.
    Original languageEnglish
    Pages (from-to)207-216
    Number of pages9
    JournalJournal of Logic Programming
    Volume28
    Issue number3
    DOIs
    Publication statusPublished - Sep 1996

    Fingerprint

    Dive into the research topics of 'A note on semantics of logic programs with equality based on complete sets of E-unifiers'. Together they form a unique fingerprint.

    Cite this