When First-order Unification Calls itself

Kód výsledku v 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>

Výsledek na webu

<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

—

Jazyk výsledku

angličtina

Název v původním jazyce

When First-order Unification Calls itself

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

When First-order Unification Calls itself

Popis výsledku anglicky

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.

Druh

O - Ostatní výsledky

CEP obor

—

OECD FORD obor

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

Projekt

—

Návaznosti

I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace

Rok uplatnění

2022

Kód důvěrnosti údajů

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