When First-order Unification Calls itself

Result code in IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F67985807%3A_____%2F22%3A00561005" target="_blank" >RIV/67985807:_____/22:00561005 - isvavai.cz</a>

Result on the web

<a href="https://www.uoh.cl/unif-2021/assets/proceedings-UNIF2021.pdf" target="_blank" >https://www.uoh.cl/unif-2021/assets/proceedings-UNIF2021.pdf</a>

DOI - Digital Object Identifier

—

Result language

angličtina

Original language name

When First-order Unification Calls itself

Original language description

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.

Czech name

—

Czech description

—

Type

O - Miscellaneous

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

—

Continuities

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Publication year

2022

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů