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

13 marca 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?)
23 stycznia 2026 12:15
Andrzej Tarlecki (MIMUW)
On the stability and fragility of interpolation (O stabilności i delikatności interpretacji)
Głównym tematem tego wystąpienia jest wersja twierdzenia Craiga o interpolacji sformułowana dla dowolnego systemu logicznego ujętego w postaci instytucji, będącej kluczowym pojęciem w rozwoju szeregu istotnych idei i wyników dotyczących podstaw specyfikacji oprogramowania oraz jego …
9 stycznia 2026 12:15
Michał Gajda (MIMUW)
Dependent types in ultrafinitistic logic (Typy zależne w logice ultrafinitystycznej)
Referat będzie raportem z obecnego stanu prac nad przełożeniem mojej Spółnej Logiki Ultrafinitystycznej (CUFL) na typy zależne (DUFL) i udowodnienia konserwatywności tego rozszerzenia w Agdzie. Dodatkowo próbuję przełożyć podsystem ograniczania złożoności termów (complexity bounds) na …
19 grudnia 2025 12:15
Michał Gajda (MIMUW)
MaxSAT and its applications (MaxSAT i jego zastosowania)
Największa Spełnialność (MaxSAT) korzysta z rozwiązywaczy spełnialności (SAT) do optymalizacji dyskretnej. Zasadą jest maksymalizacja liczby jednocześnie spełnionych reguł „opcjonalnych” (bo reguły obowiązkowe muszą być spełnione zawsze.) Umożliwia to rozwiązywanie problemów NP-trudnych, takich jak pokrycie zbiorów …
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
Aleksy Schubert (MIMUW)
(talk cancelled) ((referat usunięty))
13 czerwca 2025 12:15
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)
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 …