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

Grigoris Antoniou, Elmar Langetepe

Research output: Contribution to journalArticle

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.

LanguageEnglish
Pages229-241
Number of pages13
JournalLogic Journal of the IGPL
Volume2
Issue number2
DOIs
Publication statusPublished - 1 Sep 1994
Externally publishedYes

Fingerprint

Logic
Default Reasoning
Correctness

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 = "9",
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",

}

Applying SLD-Resolution to a Class of Non-Horn Logic Programs. / Antoniou, Grigoris; Langetepe, Elmar.

In: Logic Journal of the IGPL, Vol. 2, No. 2, 01.09.1994, p. 229-241.

Research output: Contribution to journalArticle

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 - http://www.scopus.com/inward/record.url?scp=84963057516&partnerID=8YFLogxK

U2 - 10.1093/jigpal/2.2.229

DO - 10.1093/jigpal/2.2.229

M3 - Article

VL - 2

SP - 229

EP - 241

JO - Logic Journal of the IGPL

T2 - Logic Journal of the IGPL

JF - Logic Journal of the IGPL

SN - 1367-0751

IS - 2

ER -