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

Содержательно структура описания задач и сами задачи взяты из книги [1]. Все задачи относятся к виду простых "литеральных" вычислений на структуре, т.е. не только не приводят к изменению структуры, но даже не выделяют из неё подструктур того или иного вида.

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

Важно отметить, что постановка и решение задачи может быть определено на многих языках, как естественных, так и формальных, и каркас задач открыт для новых языков. В настоящем каркасе используются русский и английский языки, YAFOLL [4], FL0. Предполагается рассмотреть язык системы поддержки доказательств Isabelle [5].

Видео доклада.

Литература:

1. Графы, сети и алгоритмы. М. «Мир» 1984. /Graphs, Networks, and Algorithms. M. N. S. Swamy, K. Thulasiraman. Wiley, 1981.
2. А. Шкотин. Каркас теории - концентратор знаний. 2023. URL: https://docs.google.com/document/d/1tZUQhaLtTzZOY5Bj-ZZ9a-wrGrnSldCFlAiia6yjY5Q/edit
3. А. Шкотин. Каркас задач. Конкретные задачи норграфии на конкретной структуре. URL: https://docs.google.com/document/d/16_pMl_w5pn8yabpP-wo-UuIYTHZ6Z1J0P0b7-_3BhpM/edit
4. А. Шкотин. Язык работы с конечными системами YAFOLL. 2015. http://dx.doi.org/10.13140/RG.2.1.4594.5046
5. Isabelle: a generic proof assistant. 2024. https://isabelle.in.tum.de/