On word unification in Coq

Prelegent(ci)

Aleksy Schubert

Afiliacja

MIMUW

Termin

20 maja 2022 12:15

Informacje na temat wydarzenia

on-line, link podaję emailem/I send link on request by email

Seminarium

Semantyka, Logika I Weryfikacja Oraz Wiele Ich Ciekawych Aplikacji

---

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 be accompanied by a presentation of what has already been proven in this direction in Coq.

---