When First-order Unification Calls itself

Authors: David M. Cerna
Publication year: 2022
Publication type: Konferenční příspěvek (mezinárodní konf.)
Periodical: Informal Proceedings of the 35th International Workshop on Unification (UNIF 2021)
Bibliographic citation: CERNA, David M. When First-order Unification Calls itself. In: BAADER, F., BAUMGARTNER, A., eds. Informal Proceedings of the 35th International Workshop on Unification (UNIF 2021). Buenos Aires, 2022, S. 1-6. Dostupné z: https://www.uoh.cl/unif-2021/assets/proceedings-UNIF2021.pdf
ID: 561005
Online record: View online record

Abstract

ZÁKLADNÍ ÚDAJE: Informal Proceedings of the 35th International Workshop on Unification (UNIF 2021). Buenos Aires, 2022 - (Baader, F., Baumgartner, A.), s. 1-6. KONFERENCE: UNIF 2021: International Workshop on Unification /35./. Buenos Aires / Virtual (AR), 18.07.2022-18.07.2022. ABSTRAKT: We present a unification problem based on first-order syntactic unification which ask whether every problem in a particular infinite sequence of unification problems is unifiable. The restricted structure of our sequence of unification problems allows an alternative formulation of the problem as recursively calling first-order syntactic unification on certain bindings if the unifier has a particular structure. The latter formulation allows us to conjecture a sufficient condition for unifiability of the sequence based on the structure of a finite sequence of unifiers. It remains an open whether this condition is also necessary.