(Higher -Order ) Equational Unification as Logic Programming

EasyChair Preprint 15677

Abstract

T his paper addresses a serious problem in the practical
implementation of (higher-order) equational unification in higher-order logical
frameworks. Naive implementations of (higher-order) equational unification in
which variables to be solved are directly represented by free logic variables
leads to non-decidability. This paper solves this problem and develops a
workable solution set. We propose an implementation of (higher-order)
equational unification in a logic programming style using lambda prolog. We
formally expose the implementation result in an abstract level, which looks
similar to standard (higher-order) equational unification rules. The design of the
formal exposition and the implementation is such that the mapping between
them is transparent. This result gives concrete and uniform framework for
(higher-order) equational unification.

Keyphrases: (higher-order) equational unification, decidability, logic programming

@booklet{EasyChair:15677,
  author    = {Murat Si̇nan Aygün},
  title     = {(Higher -Order ) Equational Unification as Logic Programming},
  howpublished = {EasyChair Preprint 15677},
  year      = {EasyChair, 2025}}