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

Anatoli Degtyarev; Andrei Voronkov

doi:10.1016/0743-1066(96)00049-0

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

Anatoli Degtyarev, Andrei Voronkov

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	207-216
Number of pages	9
Journal	Journal of Logic Programming
Volume	28
Issue number	3
DOIs	https://doi.org/10.1016/0743-1066(96)00049-0
Publication status	Published - Sep 1996

Access to Document

10.1016/0743-1066(96)00049-0

Cite this

@article{b29b921d2c9c47d3a6d7d87e35b6f735,

title = "A note on semantics of logic programs with equality based on complete sets of E-unifiers",

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.",

author = "Anatoli Degtyarev and Andrei Voronkov",

year = "1996",

month = sep,

doi = "10.1016/0743-1066(96)00049-0",

language = "English",

volume = "28",

pages = "207--216",

journal = "Journal of Logic Programming",

issn = "0743-1066",

publisher = "Elsevier BV",

number = "3",

}

TY - JOUR

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

AU - Degtyarev, Anatoli

AU - Voronkov, Andrei

PY - 1996/9

Y1 - 1996/9

N2 - 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.

AB - 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.

U2 - 10.1016/0743-1066(96)00049-0

DO - 10.1016/0743-1066(96)00049-0

M3 - Article

VL - 28

SP - 207

EP - 216

JO - Journal of Logic Programming

JF - Journal of Logic Programming

SN - 0743-1066

IS - 3

ER -

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

Abstract

Access to Document

Fingerprint

Cite this