СНАРК (доказательство теоремы)
 | Эта статья включает список литературы , связанную литературу или внешние ссылки , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . ( Май 2024 г. ) |
SNARK (Новый набор автоматизированных рассуждений SRI) — средство доказательства теорем для многосортной логики первого порядка, предназначенное для приложений в области искусственного интеллекта и разработки программного обеспечения , разработанное в SRI International .
Основными механизмами вывода SNARK являются разрешение и парамодуляция ; кроме того, он предлагает специализированные процедуры принятия решений для конкретных областей, например, решатель ограничений для логики временных интервалов Аллена. В отличие от многих других средств доказательства теорем полностью автоматизирован (неинтерактивен). SNARK предлагает множество стратегических элементов управления для настройки поведения поиска и, таким образом, настройки его производительности для конкретных приложений. Это, вместе с использованием многосортной логики и возможностями для интеграции процедур рассуждения специального назначения с выводами общего назначения, делает его особенно подходящим в качестве средства рассуждения для больших наборов утверждений.
SNARK используется в качестве компонента рассуждений в проекте НАСА по интеллектуальным системам . Он написан на Common Lisp и доступен под лицензией Mozilla Public License .
См. также
[ редактировать ]- Автоматизированное рассуждение
- Автоматизированное доказательство теорем
- Компьютерное доказательство
- Логика первого порядка
- Формальная проверка
Ссылки
[ редактировать ]- М. Стикель, Р. Уолдингер , М. Лоури, Т. Прессбургер и И. Андервуд. «Дедуктивная композиция астрономического программного обеспечения из библиотек подпрограмм». Материалы Двенадцатой Международной конференции по автоматизированному дедукции (CADE-12) , Нанси, Франция, июнь 1994 г., страницы 341–355.
- Ричард Уолдингер , Мартин Редди и Дженнифер Дунган. « Дедуктивная композиция нескольких источников данных ». Май 2002 г. Отчет о ходе выполнения исследовательской задачи по интеллектуальному пониманию данных, Проект интеллектуальной системы, NASA SISM.
- Р., Уолдингер , Д. Э. Аппельт, Дж. Фрай, Д. Д. Исраэль, П. Джарвис, Д. Мартин, С. Рихеманн, М. Е. Стикель, М. Тайсон, Дж. Хоббс и Дж. Л. Дунган. « Дедуктивный ответ на вопрос с использованием нескольких ресурсов ». в журнале « Новые направления в ответах на вопросы » , AAAI , 2004 г.
- Р. Уолдингер , П. Джарвис и Дж. Дунган. «Использование дедукции для хореографии нескольких источников данных». В книге «Семантические веб-технологии для поиска и извлечения» , остров Санибел, Флорида, октябрь 2003 г.
Внешние ссылки
[ редактировать ] | Эта статья о математическом программном незавершена обеспечении . Вы можете помочь Википедии, расширив ее . |