Organizatorzy

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

Informacje

piątki, 12:15 , sala: 5450

Dziedziny badań

Lista referatów

23 stycznia 2026 12:15
Andrzej Tarlecki (MIMUW)
Interpolation for empty carriers (Interpolacja przy pustych nośnikach)
16 stycznia 2026 12:15
Aleksy Schubert (MIMUW)
What is higher in the higher-order matching now? (Co nowego udało się dopasować w dopasowaniu wyższego rzędu?)
9 stycznia 2026 12:15
Michał Gajda (MIMUW)
Dependent types in ultrafinitistic logic (Typy zależne w logice ultrafinitystycznej)
19 grudnia 2025 12:15
Michał Gajda (MIMUW)
MaxSAT and its applications (MaxSAT i jego zastosowania)
12 grudnia 2025 12:15
Marcin Benke (MIMUW)
What is solid in the new Solidity? (Co nowego w Solidity?)
28 listopada 2025 12:15
Konrad Zdanowski (UKSW)
Strong completeness for CTL, continuation (Silne twierdzenie o pełności dla CTL, ciąg dalszy)
21 listopada 2025 12:15
Kordula Świętorzecka (UKSW)
Strong completeness for CTL (Silne twierdzenie o pełności dla CTL)
7 listopada 2025 12:15
Maurycy Wojda (MIMUW)
A Search Engine for Theorems (Wyszukiwarka twierdzeń)
24 października 2025 12:15
Paweł Balawender (MIMUW)
Reasoning about bounded arithmetic within Lean 4 (Rozumowanie o ograniczonej arytmetyce w Lean 4)
Teorie nowoczesnych asystentów dowodowych (np. Rocq, Lean, Mizar) mają bardzo dużą siłę wyrazu. Zazwyczaj jest to cecha pożądana, bo chcemy by te narzędzia były w stanie weryfikować dowody trudnych twierdzeń. Czasem jednak chcemy rozumować w …
17 października 2025 12:15
Jacek Chrząszcz (MIMUW)
What rocks in the new Rocq? (Co w nowym Rocq-u?)
Podczas seminarium opowiemy o najnowszych zmianach w The Rocq Prover, dawniej the Coq Proof Assistant. Przedstawimy w szczególności nowe elementy provera, takie jak reguły przepisywania (wreszcie ;), a także opowiemy o zmianach w elementach istniejących. …
13 czerwca 2025 12:15
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)
13 czerwca 2025 12:15
Aleksy Schubert (MIMUW)
(talk cancelled) ((referat usunięty))
6 czerwca 2025 12:15
Aleksy Schubert (MIMUW)
On equivalence in unification (O równoważności w unifikacji)
W problemie unifikacji na słowach w sposób naturalny pojawia się relacja równoważności indukowana przez zmienne i strony równania. W oparciu o tę relację możemy zdefiniować pewne pojęcie włókna, które w sposób zwięzły jednoznacznie identyfikuje pozycję …
30 maja 2025 12:15
None (MIMUW)
Talk is cancelled (Referat usunięty)
23 maja 2025 12:15
Konrad Zdanowski (UKSW)
How to Choose a Rightheous Path? In memory of Professor Pogonowski (Jak podążać dobrą drogą? Pamięci profesora Pogonowskiego)
Od dawna dużą popularnością cieszą się zagadki logiczne dotyczące kłamców, prawdomównych lub losowo odpowiadających braci, takie jak prezentuje w swoich książkach R. Smullyan. Odpowiedź polega z reguły na znalezieniu pytania, które trzeba zadać jednemu lub …