Nie jesteś zalogowany |
Powrót do listy aktywnych seminarów
Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji
Cotygodniowe seminarium badawcze.
Strona domowa: https://www.mimuw.edu.pl/~alx/piatek.html
Organizatorzy
- dr hab. Aleksy Schubert, prof. ucz.
- prof. dr hab. Andrzej Tarlecki
- prof. dr hab. Paweł Urzyczyn
Informacje
piątki, 12:15 , sala: 5450Dziedziny badań
Lista referatów
-
13 czerwca 2025 12:15
Aleksy Schubert (MIMUW)
On formalization of the higher-order matching problem (O formalizacji problemu dopasowania wyższego rzędu)
-
6 czerwca 2025 12:15
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)
-
30 maja 2025 12:15
Konrad Zdanowski (UKSW)
How to Choose a Rightheous Path? In memory of Professor Pogonowski (Jak obrać słuszną ścieżkę? Pamięci profesora Pogonowskiego)
-
23 maja 2025 12:15
Daria Walukiewicz-Chrząszcz, Jacek Chrząszcz (MIMUW)
New rewriting features of Coq (Nowe możliwości przepisywania w Coq-u)
-
16 maja 2025 12:15
Aleksy Schubert (MIMUW)
On equivalence in unification (O równoważności w unifikacji)
-
9 maja 2025 12:15
Michał Gajda
The constructive negation and postintuitionism (Konstruktywna negacja i postintuicjonizm)
-
-
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)
