You are not logged in | Log in

Speaker(s): Aleksy Schubert
Affiliation: MIMUW
Language of the talk: English
Date: Nov. 29, 2024, 12:15 p.m.
Room: room 5450
Title in Polish: Dopasowanie wyższego rzędu, transformacje T1 i T2 oraz dopasowanie czwartego rzędu
Seminar: Seminar Logic and Type Theory

Stirling's proof of the higher-order matching decidability

uses two basic solution transformations called T1 and T2

and then the third transformation called unfolding. The vocabulary

introduced on the previous talk will make it easy to formulate

the first two of them. After that I will present how to use these

to prove that the fourth-order matching is decidable.

Higher-order matching, transformations T1 and T2 and 4th order matching