Semantic Resolution for Horn Sets

Lawrence Joseph Henschen

doi:10.1109/TC.1976.1674700

Semantic Resolution for Horn Sets

Lawrence Joseph Henschen^*

^*Corresponding author for this work

Computer Science

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

5 Scopus citations

Abstract

A new resolution strategy for Horn sets of clauses, each clause of which contains no more-than one positive literal, is presented which requires. that in each resolution eitner one ancestor be a false positive unit or that one ancestor and the resolvent both be false. This strategy emphasizes “relevant” positive units while controlling the explosive nonunit resolution. Some properties of interpretations for Horn sets are reviewed and used to significantly reduce the computation and storage required to implement semantic resolution for Horn sets.

Original language	English (US)
Pages (from-to)	816-822
Number of pages	7
Journal	IEEE Transactions on Computers
Volume	C-25
Issue number	8
DOIs	https://doi.org/10.1109/TC.1976.1674700
State	Published - Aug 1976

Keywords

Horn sets
interpretations
models
resolution
semantic

ASJC Scopus subject areas

Software
Theoretical Computer Science
Hardware and Architecture
Computational Theory and Mathematics

Access to Document

10.1109/TC.1976.1674700

Cite this

@article{cd3c6daf08ce4aa9a50dbd5133a656a8,

title = "Semantic Resolution for Horn Sets",

abstract = "A new resolution strategy for Horn sets of clauses, each clause of which contains no more-than one positive literal, is presented which requires. that in each resolution eitner one ancestor be a false positive unit or that one ancestor and the resolvent both be false. This strategy emphasizes “relevant” positive units while controlling the explosive nonunit resolution. Some properties of interpretations for Horn sets are reviewed and used to significantly reduce the computation and storage required to implement semantic resolution for Horn sets.",

keywords = "Horn sets, interpretations, models, resolution, semantic",

author = "Henschen, {Lawrence Joseph}",

year = "1976",

month = aug,

doi = "10.1109/TC.1976.1674700",

language = "English (US)",

volume = "C-25",

pages = "816--822",

journal = "IEEE Transactions on Computers",

issn = "0018-9340",

publisher = "IEEE Computer Society",

number = "8",

}

TY - JOUR

T1 - Semantic Resolution for Horn Sets

AU - Henschen, Lawrence Joseph

PY - 1976/8

Y1 - 1976/8

N2 - A new resolution strategy for Horn sets of clauses, each clause of which contains no more-than one positive literal, is presented which requires. that in each resolution eitner one ancestor be a false positive unit or that one ancestor and the resolvent both be false. This strategy emphasizes “relevant” positive units while controlling the explosive nonunit resolution. Some properties of interpretations for Horn sets are reviewed and used to significantly reduce the computation and storage required to implement semantic resolution for Horn sets.

AB - A new resolution strategy for Horn sets of clauses, each clause of which contains no more-than one positive literal, is presented which requires. that in each resolution eitner one ancestor be a false positive unit or that one ancestor and the resolvent both be false. This strategy emphasizes “relevant” positive units while controlling the explosive nonunit resolution. Some properties of interpretations for Horn sets are reviewed and used to significantly reduce the computation and storage required to implement semantic resolution for Horn sets.

KW - Horn sets

KW - interpretations

KW - models

KW - resolution

KW - semantic

UR - http://www.scopus.com/inward/record.url?scp=0016983993&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0016983993&partnerID=8YFLogxK

U2 - 10.1109/TC.1976.1674700

DO - 10.1109/TC.1976.1674700

M3 - Article

AN - SCOPUS:0016983993

SN - 0018-9340

VL - C-25

SP - 816

EP - 822

JO - IEEE Transactions on Computers

JF - IEEE Transactions on Computers

IS - 8

ER -

Semantic Resolution for Horn Sets

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this