Can I read Schematic Unification on EtoBox?

Schematic Unification by Cerna, David M. is a scholarly article available to read on EtoBox.

What is Schematic Unification about?

We present a generalization of first-order unification to a term algebra where variable indexing is part of the object language. We exploit variable indexing by associating some sequences of variables ($X_0,\ X_1,\ X_2,\dots$) with a mapping $\sigma$ whose domain is the variable sequence and whose range consist of terms that may contain variables from the sequence. From a given term $t$, an infinite sequence of terms may be produced by iterative application of $\sigma$. Given a unification problem $U$ and mapping $\sigma$, the \textit{schematic unification problem} asks whether all unification problems $U$, $\sigma(U)$, $\sigma(\sigma(U))$, $\dots$ are unifiable. We provide a terminating and sound algorithm. Our algorithm is \textit{complete} if we further restrict ourselves to so-called $\infty$-stable problems. We conjecture that this additional requirement is unnecessary for completeness. Schematic unification is related to methods of inductive proof transformation by resolution and inductive reasoning.

Author

Cerna, David M.

Published

2023

Language

EN