Organizers

dr hab. Aleksy Schubert, prof. UW
prof. dr hab. Andrzej Tarlecki
prof. dr hab. Paweł Urzyczyn

Information

Fridays, 12:15 p.m. , room: 5450

Research fields

List of talks

Dec. 13, 2024, 12:15 p.m.
Jan Kostrzon (MIMUW)
Relevant S is undecidable (Nierozstrzygalność relewantnej logiki S)
I will present an article of Søren Knudstorp `Relevant S is undecidable' from LICS'24. The talk will start with a definition of semilattice models, then the lack of the finite model property will be shown …
Dec. 6, 2024, 12:15 p.m.
Aleksy Schubert (MIMUW)
Higher-order matching, unfolding and recapitulation (Dopasowanie wyższego rzędu, rozwijanie i podsumowanie)
The third transformation in Stirling's proof of the higher-order matching decidability is called unfolding. I will present its definition and I will sketch the final recapitulation of the Stirling's proof. Notably, the transformation is defined …
Nov. 29, 2024, 12:15 p.m.
Aleksy Schubert (MIMUW)
Higher-order matching, transformations T1 and T2 and 4th order matching (Dopasowanie wyższego rzędu, transformacje T1 i T2 oraz dopasowanie czwartego rzędu)
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 …
Oct. 18, 2024, 12:15 p.m.
Aleksy Schubert (MIMUW)
Stirling games in the proof of the higher-order matching problem decidability (Gry Stirlinga w dowodzie rozstrzygalności problemu dopasowania wyższego rzędu)
The initial part of the Stirling's proof that the higher order matching problem is decidable is devoted to the notion of specific game. This game approach is simply a framework in which a reduction machine …
Oct. 11, 2024, 12:15 p.m.
Aleksy Schubert (MIM)
The context of the higher-order matching problem (Kontekst problemu dopasowania wyższego rzędu)
The higher-order matching problem is a notoriously difficult decision problem, which was solved by Colin Stirling positively. However, the existing proof is very difficult to understand. I will present the basic definitions concerning the problem …
May 17, 2024, 12:15 p.m.
Konrad Zdanowski (UKSW)
A simplified lower bound for implicational logic (Uproszczona dolna granica dla logiki implikacyjnej)
A streamlined and simplified exponential lower bound on the length of proofs in intuitionistic implicational logic will be presented. The construction suffices to be adaptated to Gordeev and Haeusler’s dag-like natural deduction.
April 5, 2024, 12:15 p.m.
Michał Walicki (University of Bergen)
Paradoxes and truth in a logic of sentential operators (Paradoksy i prawda w logice operacji zdaniowych)
We show how to extend any classical (first or higher order) language with the sentential quantifiers and operators. Graph-based semantics coincides with the classical one for the classical sublanguage. The self-referential capabilities allow to express …
June 16, 2023, 12:15 p.m.
Maciej Zielenkiewicz (MIM)
Small model property in games and automata
Small model property is an important property that implies decidability. We show that the small model size is directly related to some important resources in games and automata for checking provability.
June 2, 2023, 12:15 p.m.
Aleksy Schubert (MIM)
O nierozstrzygalności wyprowadzania typów przy ograniczonej randze lub arności
W modelowaniu języków funkcyjnych z polimorfizmem ważną rolę odgrywa System F Girarda i Reynoldsa. Wiadomo, że dla termów w stylu Curry'ego, jeśli system nie jest w żaden sposób ograniczony, to wyprowadzanie typów jest nierozstrzygalne już …
May 26, 2023, 12:15 p.m.
Michał Gajda (MigaMake Pte Ltd, Singapore)
Logika ultrafinitystyczna: Filozofia i konsekwencje
Ultrafinityzm jest filozofią negującą możliwość wnioskowania o bardzo dużych liczbach. Ponieważ przedstawienie spójnej i wystarczająco mocnej logiki ultrafinitystycznej jest uważane za problem otwarty, to przedstawię reguły wnioskowania dla takiej, podważę założenia twierdzenia Goedla i opiszę …
April 28, 2023, 12:15 p.m.
Konrad Zdanowski (UKSW)
Looping proofs
Oto autorskie streszczenie referatu: Opowiem o pracy A. Atseriasa i M. Laurii, w której autorzy analizują dowody w klasycznym rachunku zdań, w których grafy dowodu mogą być cykliczne, tzn. możemy, na przykład, użyć dowodzonej …
April 21, 2023, 12:15 p.m.
Paweł Urzyczyn (MIMUW)
Substructural logics
Wiadomo, że logiki BCI i BCK są NP-zupełne. Ale jak się dobrze postawi pytanie o wnioskowanie w BCK (BCI), to odpowiedź jest całkiem inna i może być nawet akermańska. It is known that BCI and …
April 14, 2023, 12:15 p.m.
Andrzej Tarlecki (MIM)
On the fragility of interpolation
We study a version of Craig interpolation formulated in the framework of the theory of institutions. This formulation proved crucial in the development of a number of key results concerning foundations of software specification and …
March 31, 2023, 12:15 p.m.
Aleksy Schubert (MIMUW)
Overview of network protocol implementations in functional programming languages
Network protocols are usually described as dynamic processes. This does not make a perfect match with functional programming paradigm. Still, there are many initiatives to implement software artifacts in functional programming languages. This talk makes …
March 17, 2023, 12:15 p.m.
Jacek Chrząszcz (MIMUW)
News in Coq
The talk will tell us about new things that emerged in Coq and around Coq proof assistant with its new release.