Organizers

prof. dr hab. Paweł Urzyczyn

Information

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

Research fields

List of talks

April 5, 2024, 12:15 p.m.
Michał Walicki (University of Bergen)
Paradoxes and truth in a logic of sentential operators
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.
Jan. 20, 2023, 12:15 p.m.
Aleksy Schubert (MIM)
Provability of existential quantification in intuitionistic logics
The type inhabitation problem, in other terminology formula provability problem, in the second-order lambda calculus with existential quantifier and arrow will be proved during the talk to be undecidable, which contrasts with the result that …
Dec. 16, 2022, 12:15 p.m.
Paweł Urzyczyn (MIMUW)
Excavation works in my office
I will present a result of excavation works in my office, namely a forgotten theorem of Plotkin: adding fixpoint combinator to simply typed lambda-calculus does not enlarge the class of definable functions. The contents of …
Nov. 25, 2022, 12:15 p.m.
Andrzej Tarlecki (MIMUW)
not always) easy to spoi
Many results in foundations of software specification and development depend on interpolation properties of the underlying logical systems. Craig interpolation has been known to hold for first-order logic at least since the late 50ties, with …
Oct. 28, 2022, 12:15 p.m.
Daria Walukiewicz-Chrząszcz (MIMUW)
Definitional Proof Irrelevance in Coq
June 3, 2022, 12:15 p.m.
Aleksy Schubert (MIMUW)
Algorithm for proving in intuitionistic propositional logic with limited number of atoms
Na mocy twierdzenia Diego, które mówi o skończoności algebraicznego modelu wolnego dla minimalnej logiki zdaniowej, oraz jego uszczegółowień szacujących rozmiar tego modelu wiadomo, że istnieje wielomianowy algorytm rozstrzygający prawdziwość formuł minimalnej logiki zdaniowej przy założeniu, …
May 27, 2022, 12:15 p.m.
Konrad Zdanowski (UKSW)
Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter
Zostanie przedstawiona praca panów Rybakov i Shaktov, pt. Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter pokazująca nierozstrzygalność logik modalnych i intuicjonistycznych z dwoma zmiennymi i jednym unarnym …