When First-order Unification Calls itself

Description

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 for- mulation 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 con- jecture 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.

Period	18 Jul 2021
Event title	UNIF 2021
Event type	Conference
Location	AustriaShow on map