You are not logged in |
Weekly research seminar
Organizers
- dr hab. Aleksy Schubert, prof. ucz.
- prof. dr hab. Andrzej Tarlecki
- prof. dr hab. Paweł Urzyczyn
Information
Fridays, 12:15 p.m. , room: 5450Research fields
List of talks
-
June 13, 2025, 12:15 p.m.
Aleksy Schubert (MIMUW)
On formalization of the higher-order matching problem (O formalizacji problemu dopasowania wyższego rzędu)
-
June 6, 2025, 12:15 p.m.
Michał Gajda
Eldarica and Horn clause solvers (Eldarica i solvery dla klauzul Hornowskich)
-
May 30, 2025, 12:15 p.m.
Konrad Zdanowski (UKSW)
How to Choose a Rightheous Path? In memory of Professor Pogonowski (Jak obrać słuszną ścieżkę? Pamięci profesora Pogonowskiego)
-
May 23, 2025, 12:15 p.m.
Daria Walukiewicz-Chrząszcz, Jacek Chrząszcz (MIMUW)
New rewriting features of Coq (Nowe możliwości przepisywania w Coq-u)
-
May 16, 2025, 12:15 p.m.
Aleksy Schubert (MIMUW)
On equivalence in unification (O równoważności w unifikacji)
-
May 9, 2025, 12:15 p.m.
Michał Gajda
The constructive negation and postintuitionism (Konstruktywna negacja i postintuicjonizm)
-
April 25, 2025, 12:15 p.m.
Michał Gajda (MIMUW)
On foundations of mathematics (O podstawach matematyki)
-
April 11, 2025, 12:15 p.m.
Aleksy Schubert (MIMUW)
Inhabitation in System F with simple instantiations (Inhabitacja w Systemie F z prostym instancjonowaniem)
-
March 28, 2025, 12:15 p.m.
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)
I will present the results of Erfan Khaniki's work, Not All Kripke Models of HA Are Locally PA, from 2022. In this paper, the author provides a negative solution to a long-standing open problem: whether …
-
March 21, 2025, 12:15 p.m.
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)
I will present the results of Erfan Khaniki's work, Not All Kripke Models of HA Are Locally PA, from 2022. In this paper, the author provides a negative solution to a long-standing open problem: whether …
-
March 14, 2025, 12:15 p.m.
Mikołaj Konarski
Formal Mathematical Reasoning: A New Frontier in AI (Formalne rozumowanie matematyczne – nowy front w badaniach AI)
The revolution in machine learning applications has also reached research on the formalization of mathematics. In this talk, I will present an overview of contemporary achievements in this field.
-
Dec. 13, 2024, 12:15 p.m.
Jan Kostrzon (MIMUW)
Relevant S is undecidable (Nierozstrzygalność relewantnej logiki S)
I will present an article of Søren Knudstorp `Relevant S is undecidable' from LICS'24. The talk will start with a definition of semilattice models, then the lack of the finite model property will be shown …
-
Dec. 6, 2024, 12:15 p.m.
Aleksy Schubert (MIMUW)
Higher-order matching, unfolding and recapitulation (Dopasowanie wyższego rzędu, rozwijanie i podsumowanie)
The third transformation in Stirling's proof of the higher-order matching decidability is called unfolding. I will present its definition and I will sketch the final recapitulation of the Stirling's proof. Notably, the transformation is defined …
-
Nov. 29, 2024, 12:15 p.m.
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)
Stirling's proof of the higher-order matching decidability uses two basic solution transformations called T1 and T2 and then the third transformation called unfolding. The vocabulary introduced on the previous talk will make it easy to …
-
Oct. 18, 2024, 12:15 p.m.
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)
The initial part of the Stirling's proof that the higher order matching problem is decidable is devoted to the notion of specific game. This game approach is simply a framework in which a reduction machine …
