You are not logged in |
Weekly research seminar
Organizers
- dr hab. Aleksy Schubert, prof. ucz.
- prof. dr hab. Andrzej Tarlecki
- prof. dr hab. Paweł Urzyczyn
Information
Fridays, 12:15 p.m. , room: 5450Research fields
List of talks
-
Jan. 23, 2026, 12:15 p.m.
Andrzej Tarlecki (MIMUW)
Interpolation for empty carriers (Interpolacja przy pustych nośnikach)
-
Jan. 16, 2026, 12:15 p.m.
Aleksy Schubert (MIMUW)
What is higher in the higher-order matching now? (Co nowego udało się dopasować w dopasowaniu wyższego rzędu?)
-
Jan. 9, 2026, 12:15 p.m.
Michał Gajda (MIMUW)
Dependent types in ultrafinitistic logic (Typy zależne w logice ultrafinitystycznej)
-
Dec. 19, 2025, 12:15 p.m.
Michał Gajda (MIMUW)
MaxSAT and its applications (MaxSAT i jego zastosowania)
-
Dec. 12, 2025, 12:15 p.m.
Marcin Benke (MIMUW)
What is solid in the new Solidity? (Co nowego w Solidity?)
-
Nov. 28, 2025, 12:15 p.m.
Konrad Zdanowski (UKSW)
Strong completeness for CTL, continuation (Silne twierdzenie o pełności dla CTL, ciąg dalszy)
-
Nov. 21, 2025, 12:15 p.m.
Kordula Świętorzecka (UKSW)
Strong completeness for CTL (Silne twierdzenie o pełności dla CTL)
We will discuss the history of the development of Prior’s temporal logics, which are now used in computer science. Our main focus will be the branching-time logic CTL. We will examine issues related to completeness …
-
Nov. 7, 2025, 12:15 p.m.
Maurycy Wojda (MIMUW)
A Search Engine for Theorems (Wyszukiwarka twierdzeń)
-
Oct. 24, 2025, 12:15 p.m.
Paweł Balawender (MIMUW)
Reasoning about bounded arithmetic within Lean 4 (Rozumowanie o ograniczonej arytmetyce w Lean 4)
The theories of modern proof assistants (e.g. Rocq, Lean, Mizar) are highly expressive. This is usually a desirable feature, since we want these tools to be capable of verifying proofs of complex theorems. However, sometimes …
-
Oct. 17, 2025, 12:15 p.m.
Jacek Chrząszcz (MIMUW)
What rocks in the new Rocq? (Co w nowym Rocq-u?)
In the talk, we will present the latest changes in The Rocq Prover, formerly known as the Coq Proof Assistant. In particular, we will present new features of the prover, such as rewriting rules (at …
-
June 13, 2025, 12:15 p.m.
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)
-
-
June 6, 2025, 12:15 p.m.
Aleksy Schubert (MIMUW)
On equivalence in unification (O równoważności w unifikacji)
-
-
May 23, 2025, 12:15 p.m.
Konrad Zdanowski (UKSW)
How to Choose a Rightheous Path? In memory of Professor Pogonowski (Jak podążać dobrą drogą? Pamięci profesora Pogonowskiego)
Everyone is familiar with Smullyan-like riddles where there are some twin brothers, liars, truth-tellers or random-tellers, and we must question them to decide the correct way. We present a way of formalizing such riddles in …
