TPTP World Infrastructure for Non-classical Logics

## Контекст Область автоматизированного доказательства теорем (ATP) является ключевым направлением в искусственном интеллекте и логике, нацеленным на создание систем, автоматически доказывающих теоремы в различных областях математики, информатики и других наук. Одной из ведущих платформ в этой области является TPTP World, которая создана для поддержки развития и исследований в области ATP. Тем не менее, до начала 2010-х годов TPTP World основывалась исключительно на классических логиках. С появлением версии 9.0.0 появилась возможность работы с неклассическими логиками, что открыло новые возможности для изучения и применения логических систем. Однако, несмотря на эту новую возможность, подробное описание инфраструктуры TPTP World для неклассических логик отсутствовало до текущей работы. ## Метод Предлагаемая работа представляет собой детальное описание функциональности TPTP World для неклассических логик. Рассматривается расширение языка TPTP для поддержки неклассических логик, включая спецификацию проблем, решений и методов доказательства. Также описывается инфраструктура, включая архитектуру и технические решения, позволяющие эффективно использовать TPTP World для неклассических логик. Особое внимание уделяется описанию инструментов, которые поддерживают работу с неклассическими логиками, в том числе инструментов для вывода, проверки и оценки решений. Эта работа также охватывает детальный анализ использования TPTP World для доказательства теорем в определенной логике, такой как высказывательная логика с квантификацией. ## Результаты Исследования показали, что TPTP World эффективно может работать с неклассическими логиками, предоставляя всестороннюю инфраструктуру для разработки, тестирования и применения систем автоматического доказательства. Были проведены эксперименты с различными логическими системами и проблемами, чтобы продемонстрировать возможности системы. Например, был проведен эксперимент с логикой нормальных квантификаций, где было доказано несколько теорем с помощью TPTP World. Результаты этих экспериментов показали, что TPTP World обеспечивает высокую точность и эффективность в работе с неклассическими логиками. ## Значимость Предлагаемый подход имеет широкие области применения в математике, информатике, физике и других науках, где требуется использование автоматических систем доказательства для неклассических логик. Также TPTP World может быть полезен для разработчиков и исследователей, которые используют неклассические логики в своих исследованиях. Одним из основных преимуществ является возможность эффективного использования существ