DocumentCode
1399210
Title
A theory of unification
Author
Vadera, Sunil
Author_Institution
Dept. of Math. & Comput. Sci., Salford Univ., UK
Volume
3
Issue
5
fYear
1988
fDate
9/1/1988 12:00:00 AM
Firstpage
149
Lastpage
160
Abstract
Unification is an important concept. It is used in Prolog, resolution, term rewriting and natural language understanding. As the use of formal methods increases, unification will be part of formally developed systems. Hence a theory of unification is desirable. The paper demonstrates the use of the Vienna Development Method (VDM) to develop a theory of unification. Substitution application is defined recursively, a theory of non-circular substitutions is developed, and an implicit specification of unification is written. A proof of a particular unification is outlined with respect to this specification. The algorithm considered is more space-efficient than that which Manna and Waldinger (1981) prove correct. The theory developed is also compared with that of Manna and Waldinger
Keywords
data structures; formal logic; program verification; programming theory; VDM; Vienna Development Method; data structures; formal logic; program verification; programming theory; space-efficient; unification;
fLanguage
English
Journal_Title
Software Engineering Journal
Publisher
iet
ISSN
0268-6961
Type
jour
Filename
6903
Link To Document