LEGO (помощник доказательства)
LEGO — это помощник для доказательства, разработанный Рэнди Поллаком из Эдинбургского университета . Он реализует несколько теорий типов: Эдинбургскую логическую структуру (LF), Исчисление конструкций (CoC), Обобщенное исчисление конструкций (GCC) и Единую теорию зависимых типов (UTT). [1]
Ссылки [ править ]
- ^ «Поиск программного обеспечения — zbMATH Open» . zbmath.org . Проверено 3 ноября 2022 г.