Каркас теории и каркас задач

Авторы и предъявление

Минутная экспозиция

Каркас теории предлагает хранить существенные элементы отдельной предметной теории в одном поддерживаемом месте: структуру моделей, аксиомы, определения терминов, свойства моделей, гипотезы, теоремы и доказательства. [E]

Его цель - концентрация и проверка знания, после которой теория легче формализуется, записывается математически и передается в алгоритмическую обработку. [E]

Примером служит теория неориентированных графов: элементы структуры получают идентификаторы, формулировки даются на русском, английском и формальных языках, а доказательство раскладывается на шаги с предпосылками и методами вывода. [E]

Каркас задач добавляет прикладной слой: постановки и решения задач хранятся в структурированной форме, а формализованные рассуждения могут быть переданы процессору для проверки истинности. [E]

Программа тем самым соединяет методологию научного знания, формальные языки, онтологическое представление и инженерную проверку рассуждений. [E]

Ключевые конструкты

Основания и обязательства

• Методологическое обязательство программы состоит в том, что теория предметной области должна быть представима как поддерживаемый общий каркас, а не только как множество разрозненных текстов. [E]
• Формализация не отменяет естественный язык: русские и английские формулировки сосуществуют с YAFOLL, FL0 и потенциально с языками систем доказательства. [E]
• Эпистемическое обязательство - проверяемость переходов: гипотезы должны получать доказательства, доказательства раскладываются на шаги, а формализованные рассуждения передаются на проверку. [E]
• Инженерная ставка сделана на извлечение элементов теории под конкретную задачу: элементы каркаса могут встраиваться в документы и собираться для решения практических задач. [E]
• YAFOLL образует один из языковых предшественников программы, потому что задает язык работы с конечными алгебраическими системами и математическими моделями частей реальности. [E]
• Граница доказательности проходит по публичной реализации: источники подтверждают программу, примеры и прототипную инфраструктуру, но не подтверждают зрелую открытую платформу с воспроизводимыми командами проверки. [E]

Операционная состоятельность

• Уровень O1 .
• Операциональные конструкции зафиксированы: нужно выделять структуру моделей, аксиомы, определения, гипотезы, теоремы и доказательства; каждому блоку давать идентификатор; хранить многоязычные формулировки; связывать употребления терминов с блоками; раскладывать доказательство на шаги с предпосылками и методами вывода. [E]
• Каркас задач добавляет действие для пользователя: поставить задачу в предметной области, найти в каркасе похожую задачу, использовать структурированную постановку и решение, передать формализованное рассуждение процессору для проверки. [E]
• Уровень не выше O1 , потому что перенос вне авторского прототипа не зафиксирован. Письмо в Isabelle-сообщество показывает намерение наполнять каркас из Isabelle и сделать каркас механики, но не документирует независимую эксплуатацию. [E]
• Уровень является маркером применимости корпуса, а не оценкой ценности программы.

Зрелость

• Зрелость: ранняя инженерно-методологическая программа.
• Основание: публичный корпус уже включает доклад Formal Philosophy 2023, презентацию о каркасе теории, семинарный доклад о каркасе задач и письмо в сообщество Isabelle. [E]
• Устойчивость темы прослеживается в повторении одной линии: теория как каркас знания, пример неориентированных графов, многоязычная формализация, извлечение элементов каркаса для задач и планы подключения систем доказательства. [E]
• До разработанной программы не хватает опубликованной спецификации формата, открытого репозитория или устойчивой платформы, независимого использования, авторской сверки статуса Google Docs-прототипов и ясной границы между “каркасом теории” и “каркасом задач”. [E]

Прототипы и инженерные реализации

• Прототипная поверхность каркаса теории зафиксирована в презентации: каркас неориентированных графов хранится в Google Docs, открыт для комментирования и используется как пример встраивания элементов каркаса в документ. [E]
• Прототипная поверхность каркаса задач зафиксирована в докладе о норграфии: постановки и решения задач представлены в структурированной форме, а языковая поверхность включает русский, английский, YAFOLL и FL0. [E]
• Письмо в Isabelle-архиве фиксирует следующий инженерный маршрут: наполнение каркаса из Isabelle, создание каркаса механики и использование Coq, Isabelle, HOL4 и других формальных языков в формальных онтологиях. [E]
• Реализации пока подтверждены как авторские демонстрационные контуры. Открытый код, формат данных, процессор проверки, команды запуска и внешняя репликация не зафиксированы. [E]

Связанные профили

не обнаружено

Корпус и свидетельства

Состояние профиля

• Состояние: профиль собран. [E]
• Подтверждено: публичное название доклада, программа каркаса теории, пример неориентированных графов, многоязычная структура блоков, роль определений, гипотез, теорем и доказательств, каркас задач для норграфии и связь с системами доказательства. [E]
• Слабо подтверждено: границы канонического корпуса Google Docs, состояние прототипа, наличие процессора проверки, актуальная реализация, независимое использование и точное публичное имя автора в русской форме.
• Блокеры перед усилением статуса: авторская сверка названия и границ программы, проверка Google Docs-артефактов, поиск репозитория или формата данных, проверка воспроизводимого сценария, разбор отношения каркаса задач к каркасу теории и поиск публичных ссылок на релевантные Telegram-сообщения.