Applying SLD-Resolution to a Class of Non-Horn Logic Programs

Grigoris Antoniou; Elmar Langetepe

doi:10.1093/jigpal/2.2.229

Applying SLD-Resolution to a Class of Non-Horn Logic Programs

Grigoris Antoniou, Elmar Langetepe

University of Osnabrück

Research output: Contribution to journal › Article › peer-review

3 Citations (Scopus)

Abstract

Methods for dealing with a Horn logic program and one goal are well-known and successful. Here we are concerned with treating logic programa enhanced by some negative literals using the same methods, in particular SLD-resolutlon. We describe the approach and show it. correctness. The result can be applied to default reasoning and has some relevance for model elimination based theorem proving.

Original language	English
Pages (from-to)	229-241
Number of pages	13
Journal	Logic Journal of the IGPL
Volume	2
Issue number	2
DOIs	https://doi.org/10.1093/jigpal/2.2.229
Publication status	Published - 1 Sept 1994
Externally published	Yes

Access to Document

10.1093/jigpal/2.2.229Licence: Unspecified

Cite this

@article{af6fbae75f404b1b8e915dbfbfd1a042,

title = "Applying SLD-Resolution to a Class of Non-Horn Logic Programs",

abstract = "Methods for dealing with a Horn logic program and one goal are well-known and successful. Here we are concerned with treating logic programa enhanced by some negative literals using the same methods, in particular SLD-resolutlon. We describe the approach and show it. correctness. The result can be applied to default reasoning and has some relevance for model elimination based theorem proving.",

keywords = "Default reasoning, Logic programming, Model elimination, Theorem proving",

author = "Grigoris Antoniou and Elmar Langetepe",

year = "1994",

month = sep,

day = "1",

doi = "10.1093/jigpal/2.2.229",

language = "English",

volume = "2",

pages = "229--241",

journal = "Logic Journal of the IGPL",

issn = "1367-0751",

publisher = "Oxford University Press",

number = "2",

}

TY - JOUR

T1 - Applying SLD-Resolution to a Class of Non-Horn Logic Programs

AU - Antoniou, Grigoris

AU - Langetepe, Elmar

PY - 1994/9/1

Y1 - 1994/9/1

N2 - Methods for dealing with a Horn logic program and one goal are well-known and successful. Here we are concerned with treating logic programa enhanced by some negative literals using the same methods, in particular SLD-resolutlon. We describe the approach and show it. correctness. The result can be applied to default reasoning and has some relevance for model elimination based theorem proving.

AB - Methods for dealing with a Horn logic program and one goal are well-known and successful. Here we are concerned with treating logic programa enhanced by some negative literals using the same methods, in particular SLD-resolutlon. We describe the approach and show it. correctness. The result can be applied to default reasoning and has some relevance for model elimination based theorem proving.

KW - Default reasoning

KW - Logic programming

KW - Model elimination

KW - Theorem proving

UR - https://www.scopus.com/pages/publications/84963057516

U2 - 10.1093/jigpal/2.2.229

DO - 10.1093/jigpal/2.2.229

M3 - Article

AN - SCOPUS:84963057516

SN - 1367-0751

VL - 2

SP - 229

EP - 241

JO - Logic Journal of the IGPL

JF - Logic Journal of the IGPL

IS - 2

ER -

Applying SLD-Resolution to a Class of Non-Horn Logic Programs

Abstract

Access to Document

Other files and links

Fingerprint

Cite this