Schematic Unification
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2023
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909132974456832 |
|---|---|
| author | Cerna, David M. |
| author_facet | Cerna, David M. |
| contents | 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 $σ$ 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 $σ$. Given a unification problem $U$ and mapping $σ$, the \textit{schematic unification problem} asks whether all unification problems $U$, $σ(U)$, $σ(σ(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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2306_09152 |
| institution | arXiv |
| publishDate | 2023 |
| record_format | arxiv |
| spellingShingle | Schematic Unification Cerna, David M. Logic in Computer Science 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 $σ$ 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 $σ$. Given a unification problem $U$ and mapping $σ$, the \textit{schematic unification problem} asks whether all unification problems $U$, $σ(U)$, $σ(σ(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. |
| title | Schematic Unification |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2306.09152 |