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

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)
11 października 2024 12:15
Aleksy Schubert (MIM)
The context of the higher-order matching problem (Kontekst problemu dopasowania wyższego rzędu)
17 maja 2024 12:15
Konrad Zdanowski (UKSW)
Uproszczona dolna granica dla logiki implikacyjnej (A simplified lower bound for implicational logic)
5 kwietnia 2024 12:15
Michał Walicki (University of Bergen)
Paradoksy i prawda w logice operacji zdaniowych (Paradoxes and truth in a logic of sentential operators)
16 czerwca 2023 12:15
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.
2 czerwca 2023 12:15
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ż …