СНАРК (доказательство теорем)

Эта статья включает список ссылок , связанных материалов или внешних ссылок , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . Пожалуйста, помогите улучшить эту статью, введя более точные цитаты. ( Май 2024 ) ( Узнайте, как и когда удалить это сообщение )

SNARK (новый автоматизированный набор для рассуждений SRI) — это средство доказательства теорем для многосортной логики первого порядка, предназначенное для приложений в области искусственного интеллекта и разработки программного обеспечения , разработанное в SRI International .

Основными механизмами вывода SNARK являются разрешение и парамодуляция ; кроме того, он предлагает специализированные процедуры принятия решений для определенных областей, например, решатель ограничений для временной интервальной логики Аллена. В отличие от многих других доказателей теорем, он полностью автоматизирован (неинтерактивен). SNARK предлагает множество стратегических элементов управления для корректировки своего поведения поиска и, таким образом, настройки своей производительности на определенные приложения. Это, вместе с использованием им многосортной логики и возможностей для интеграции процедур рассуждения специального назначения с выводом общего назначения, делает его особенно подходящим в качестве рассуждения для больших наборов утверждений.

SNARK используется как компонент рассуждения в проекте NASA Intelligent Systems Project . Он написан на Common Lisp и доступен по лицензии Mozilla Public License .

• Автоматизированное рассуждение
• Автоматизированное доказательство теорем
• Компьютерное доказательство
• Логика первого порядка
• Формальная проверка

• M. Stickel, R. Waldinger , M. Lowry, T. Pressburger и I. Underwood. «Дедуктивная композиция астрономического программного обеспечения из библиотек подпрограмм». Труды Двенадцатой международной конференции по автоматизированной дедукции (CADE-12) , Нанси, Франция, июнь 1994 г., стр. 341–355.
• Ричард Уолдингер , Мартин Редди и Дженнифер Данган. «Дедуктивная композиция множественных источников данных». Отчет о ходе выполнения исследовательской задачи по интеллектуальному пониманию данных за май 2002 г., проект «Интеллектуальные системы», NASA SISM.
• R, Waldinger , DE Appelt, J. Fry, DJ Israel, P. Jarvis, D. Martin, S. Riehemann, ME Stickel, M. Tyson, J. Hobbs и JL Dungan. «Дедуктивный ответ на вопрос из нескольких источников». в New Directions in Question Answering , AAAI , 2004.
• Р. Уолдингер , П. Джарвис и Дж. Дунган. «Использование дедукции для управления несколькими источниками данных». В Semantic Web Technologies for Searching and Retrieving , Sanibel Island, Florida, октябрь 2003 г.

• Домашняя страница SNARK на сайте SRI
• Учебник СНАРК

Эта статья о математическом программном обеспечении — заглушка . Вы можете помочь Википедии, расширив ее.

• в
• т
• е