 You are not logged in | log in |
| You are not logged in | log in |
Weekly research seminar
2023-03-17, 12:15, 5820
Jacek Chrząszcz (MIMUW)
The talk will tell us about new things that emerged in Coq and around Coq proof assistant with its new release. ...
2023-01-20, 12:15, 5820
Aleksy Schubert (MIM)
Provability of existential quantification in intuitionistic logics
The type inhabitation problem, in other terminology formula provability problem, in the second-order lambda calculus with existential quantifier and arrow will be proved during the talk to be undecidable, which contrasts with the result that the second-order lambda calculus with existential quantifi...
2022-12-16, 12:15, 5820
Paweł Urzyczyn (MIMUW)
I will present a result of excavation works in my office, namely a forgotten theorem of Plotkin: adding fixpoint combinator to simply typed lambda-calculus does not enlarge the class of definable functions. The contents of the 1982 handwritten note was demonstrated at the occasion of the 9...
2022-11-25, 12:15, 5820
Andrzej Tarlecki (MIMUW)
Interpolation is (not always) easy to spoil
Many results in foundations of software specification and development depend on interpolation properties of the underlying logical systems. Craig interpolation has been known to hold for first-order logic at least since the late 50ties, with well studied links to other crucial properties, li...
2022-10-28, 12:15, 5820
Daria Walukiewicz-Chrząszcz (MIMUW)
2022-06-03, 12:15, online, wysyłam link po zgłoszeniu emailem
Aleksy Schubert (MIMUW)
Algorithm for proving in intuitionistic propositional logic with limited number of atoms
Na mocy twierdzenia Diego, które mówi o skończoności algebraicznego modelu wolnego dla minimalnej logiki zdaniowej, oraz jego uszczegółowień szacujących rozmiar tego modelu wiadomo, że istnieje wielomianowy algorytm rozstrzygający prawdziwość formuł minimalnej logiki z...
2022-05-27, 12:15, on-line, link sent by email
Konrad Zdanowski (UKSW)
Zostanie przedstawiona praca panów Rybakov i Shaktov, pt. Undecidability of First-Order Modal and Intuitionistic Logics with Two Variables and One Monadic Predicate Letter pokazująca nierozstrzygalność logik modalnych i intuicjonistycznych z dwoma zmiennymi i jednym unarnym symbolem re...
2022-05-20, 12:15, on-line, link podaję emailem/I send link on request by email
Aleksy Schubert (MIMUW)
W trakcie referatu przedstawiony zostanie szkic dowodu poprawności podstawowych własności algorytmu znajdowania unifikatorów na słowach oraz zakres jego formalizacji w Coq-u. A sketch of algorithm correctness for an algorithm to solve word unification problem will be presented. This will...
2022-05-13, 12:15, 5820
Marcin Benke (MIMUW)
Jedną z istotnych zalet czystych języków funkcyjnych, takich jak Haskell jest możliwość równościowego wnioskowania o programach. Jednakże do tej pory takie wnioskowanie miało charakter zewnętrzny względem programu: już to (najczęściej) ręcznie „na papierze”...
2022-03-25, 12:15, 5820
Jacek Chrząszcz (MIMUW)
Na referacie przedstawione zostaną ostatnie dodatki do narzędzia do dowodzenia twierdzeń Coq. ...
