Provskell
Проект включает калькулятор арифметических выражений над ординалами и прувер, позволяющий интерактивно исследовать завершаемость систем переписывания термов путём подбора их интерпретации в ординальной алгебре. Проект основан на дипломной работе Пискунова Александра (бакалавриат, выпуск 2022 года)
Ординальный калькулятор
Результат
Введите выражение и нажмите "Привести к КНФ", чтобы получить результат
Интерактивный прувер
Система переписывания термов
Интерпретация в ординальной алгебре
Определите систему переписывания термов, чтобы продолжить
Результат
Определите систему переписывания термов и подберите ее интерпретацию в ординальной алгебре, чтобы получить результат