Unification as a Simple Theorem Prover

EasyChair Preprint 15904

Abstract

In this paper, unification is considered as a simple theorem
prover in which variables to be solved are directly represented by free
logic variables. This approach is different from other works which consider
unification as the application of a set of rewrite rules. The benefit of
the approach this paper considers is naturalness, clearness and uniform
framework. The theorem prover is not in full setting. Since programming
formulas are fixed and simple a few rules, goal formulas are matched with
the left hand-side of rewrite rules. The theorem prover acts like a term
rewriting system. But when free logic variables are at the top, they are
subject to search. This paper considers the solution of this technical
problem.

Keyphrases: The most general substitution, nondeterminism, term rewriting, theorem prover, unification

@booklet{EasyChair:15904,
  author    = {Murat Sinan Aygün},
  title     = {Unification as a Simple Theorem Prover},
  howpublished = {EasyChair Preprint 15904},
  year      = {EasyChair, 2025}}