Open AccessHigher-order and semantic unification
Author(s) -
Nachum Dershowitz,
Subrata Mitra
Publication year - 1993
Publication title -
lecture notes in computer science
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.249
H-Index - 400
eISSN - 1611-3349
pISSN - 0302-9743
ISBN - 3-540-57529-4
DOI - 10.1007/3-540-57529-4_49
Subject(s) - unification , decidability , axiom , computer science , transformation (genetics) , satisfiability , set (abstract data type) , algebra over a field , theoretical computer science , discrete mathematics , algorithm , programming language , mathematics , pure mathematics , biochemistry , chemistry , geometry , gene
We provide a complete system of transformation rules for se- mantic unification with respect to theories defined by convergent rewrite systems. We show that this standard unification procedure, with slight modifications, can be used to solve the satisfiability problem in combina- tory logic with a convergent set of algebraic axioms R, thus resulting in a complete higher-order unification procedure for R. Furthermore, we use the system of transformation rules to provide a syntactic characterization for R which results in decidability of semantic unification.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom