An Algorithm for the Retrieval of Unifiers from Discrimination Trees

Hans De Nivelle

doi:10.1023/a:1005992522805

An Algorithm for the Retrieval of Unifiers from Discrimination Trees

Hans De Nivelle

Centrum voor Wiskunde en Informatica

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

1 Citation (Scopus)

Abstract

We present a modification of the unification algorithm that is adapted to the extraction of simultaneously unifiable literals from discrimination trees. The algorithm is useful for efficient implementation of binary resolution, hyperresolution, and paramodulation. The algorithm is able to traverse simultaneously more than one discrimination tree and to construct a unifier at the same time. In this way backtracking is reduced.

Original language	English
Pages (from-to)	5-25
Number of pages	21
Journal	Journal of Automated Reasoning
Volume	20
Issue number	1-2
DOIs	https://doi.org/10.1023/a:1005992522805
Publication status	Published - 1998
Externally published	Yes

Keywords

Discrimination trees
Implementation
Unification

ASJC Scopus subject areas

Software
Computational Theory and Mathematics
Artificial Intelligence

Access to Document

10.1023/a:1005992522805

Cite this

@article{3cde9a8ed9ea4d3786fbfd0e466a575c,

title = "An Algorithm for the Retrieval of Unifiers from Discrimination Trees",

abstract = "We present a modification of the unification algorithm that is adapted to the extraction of simultaneously unifiable literals from discrimination trees. The algorithm is useful for efficient implementation of binary resolution, hyperresolution, and paramodulation. The algorithm is able to traverse simultaneously more than one discrimination tree and to construct a unifier at the same time. In this way backtracking is reduced.",

keywords = "Discrimination trees, Implementation, Unification",

author = "\{De Nivelle\}, Hans",

year = "1998",

doi = "10.1023/a:1005992522805",

language = "English",

volume = "20",

pages = "5--25",

journal = "Journal of Automated Reasoning",

issn = "0168-7433",

publisher = "Springer Netherlands",

number = "1-2",

}

TY - JOUR

T1 - An Algorithm for the Retrieval of Unifiers from Discrimination Trees

AU - De Nivelle, Hans

PY - 1998

Y1 - 1998

N2 - We present a modification of the unification algorithm that is adapted to the extraction of simultaneously unifiable literals from discrimination trees. The algorithm is useful for efficient implementation of binary resolution, hyperresolution, and paramodulation. The algorithm is able to traverse simultaneously more than one discrimination tree and to construct a unifier at the same time. In this way backtracking is reduced.

AB - We present a modification of the unification algorithm that is adapted to the extraction of simultaneously unifiable literals from discrimination trees. The algorithm is useful for efficient implementation of binary resolution, hyperresolution, and paramodulation. The algorithm is able to traverse simultaneously more than one discrimination tree and to construct a unifier at the same time. In this way backtracking is reduced.

KW - Discrimination trees

KW - Implementation

KW - Unification

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

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

U2 - 10.1023/a:1005992522805

DO - 10.1023/a:1005992522805

M3 - Article

AN - SCOPUS:0032045367

SN - 0168-7433

VL - 20

SP - 5

EP - 25

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

IS - 1-2

ER -

An Algorithm for the Retrieval of Unifiers from Discrimination Trees

Abstract

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this