Applied logician, symbolic AI researcher

На данный момент null.

Мои компетенции и опыт

TL;DR Концептуальный нализ некоего X и дальнейшая проработка с реализацией X формальными методами, погружаясь вплоть до программирования на C-подобных языках.

Интересуюсь символической логикой, теориями типов и некоторыми математическими средствами, которые выглядят важными: symbolic learning, topological data analysis, algebraic invariant theory и некоторые другие.

Сначала мы работаем над формализацией некоторой концепции, идеи и затем составляем некоторую концептуальную систему о том, какие средства нам нужно сюда приложить.

Затем каждую часть концептуальной системы мы рассматриваем независимо. Обычно, если это логика, на деле это должно пройти сквозь изменения по причинам:
- устранения logical omniscience через дополнение теорией сложности;
- введения логической отменяемости (defeasible reasoning) в случае неоперативно получаемых доказательств в реальном времени;
- накладывания ограничений (budget constraint) и учёта ресурсов (abstract resource semantics);
- учёта неоднозначности вокруг (uncertainty quantification);
- улучшения логики как таковой для получения продуктивности и достижения приемлемого класса сложности.

Затем мы должны переписать это в некоторую программную металогику: Coq, Arend, Isabelle / HOL или нечто иное. Там мы сможем точнее изучить, вычислительно, формальные свойства полученной логики.

При использовании зависимых типов мы можем некоторые доказательства в реальном времени перевести теоремы, и в compile-time мы будем иметь совершенно простой алгоритм - вместо вычислений в run-time.

Чтобы был автовывод в реальном времени, требуется написать либо небольшой солвер или использовать λProlog или ACL2 для передачи управления им.

Guile работает как клей.

Мы можем поизучать поведение логики через теорию автоматов и агентное матмоделирование. Для этого надо получить динамическую семантику вплоть до императивной программы, затем ввести instruction dependency. Пишем краткую DSL, отображающую эти процедуры, задаём постулаты, смотрим на поведение.

Считаю важным также натурализовать логику: устанавливаем критерии истинности, как-либо сводящиеся к наблюдениям, и на реальном тестовом проекте смотрим, как текут доказательства и совпадают ли наши теоретические ожидания с наблюдениями.

Далее переводим этот DSL в ЯП, оптимизируя в нём код. На этом этапе логика полностью сводится к обычной программе.

В конце нужно узнать о комбинации логических программ как друг другу не противоречащих. Эту задачу можно решить можно решить через семантику расслоения Габбая (fibring semantics).

Если нужна подробная концептуализация идей и их формальная спецификация, а также формальная верификация решений в ходе работы системы, с учётом отменяемости, то это всё по этой теме.