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 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)
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 …
9 maja 2025 12:15
Michał Gajda
The constructive negation and postintuitionism (Konstruktywna negacja i postintuicjonizm)
Spróbuję w skondensowany sposób przedstawić logikę ultrafinistyczną z kwantyfikatorami (uniwersalnym i egzystencjalnym) jako rozwinięcie wcześniejszych wników opublikowanych w pracy https://drops.dagstuhl.de/enti<wbr></wbr>ties/document/10.4230/LIPIcs.<wbr></wbr>TYPES.2023.5. Oprócz kwantyfikatorów dodana zostanie również równość. Pokażę też, jak zakodować abstrakcyjne typy danych. Na koniec …
25 kwietnia 2025 12:15
Michał Gajda (MIMUW)
On foundations of mathematics (O podstawach matematyki)
11 kwietnia 2025 12:15
Aleksy Schubert (MIMUW)
Inhabitation in System F with simple instantiations (Inhabitacja w Systemie F z prostym instancjonowaniem)
Rozważany będzie fragment Systemu F, w którym kwantyfikatory ogólne mogą pojawiać sie tylko na negatywnych pozycjach, a zmienne zdaniowe mogą być instancjonowane tylko przez typy proste. Pokazane zostanie, że problem inhabitacji dla tego fragmentu jest …
28 marca 2025 12:15
Konrad Zdanowski (UKSW)
Not all Kripke models of HA are locally PA, part II (Nie wszystkie modele arytmetyki Heytinga spełniają lokalnie artytmetykę Peano, część II)
Zreferuję wyniki pracy Erfan Khanikiego, Not All Kripke models of HA are locally PA, z roku 2022. Autor rozwiązuje w niej negatywnie długo otwarty problem, czy każdy model arytmetyki Heytinga ma, jako światy w modelu …
21 marca 2025 12:15
Konrad Zdanowski (UKSW)
Not all Kripke models of HA are locally PA, part I (Nie wszystkie modele arytmetyki Heytinga spełniają lokalnie artytmetykę Peano, część I)
Zreferuję wyniki pracy Erfan Khanikiego, Not All Kripke models of HA are locally PA, z roku 2022. Autor rozwiązuje w niej negatywnie długo otwarty problem, czy każdy model arytmetyki Heytinga ma, jako światy w modelu …
14 marca 2025 12:15
Mikołaj Konarski
Formal Mathematical Reasoning: A New Frontier in AI (Formalne rozumowanie matematyczne – nowy front w badaniach AI)
Rewolucja zastosowań uczenia maszynowego dotarła również do badań nad formalizowaniem matematyki. W referacie przedstawię przegląd współczesnych osiągnięć w tej dziedzinie.
13 grudnia 2024 12:15
Jan Kostrzon (MIMUW)
Relevant S is undecidable (Nierozstrzygalność relewantnej logiki S)
W swoim wystąpieniu zreferuję artykuł Sørena Knudstorpa pt. „Relevant S is undecidable” z LICS'24. Zacznę od podania definicji modeli półkratowych, następnie pokażę dowód, że logika S nie ma własności modelu skończonego (Finite Model Property). Na …
6 grudnia 2024 12:15
Aleksy Schubert (MIMUW)
Higher-order matching, unfolding and recapitulation (Dopasowanie wyższego rzędu, rozwijanie i podsumowanie)
29 listopada 2024 12:15
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)
18 października 2024 12:15
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)