Prelegent: Aleksy Schubert

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.