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

СНАРК (Новый набор автоматизированных рассуждений SRI), это средство доказательства теорем для мульти-сортировки логика первого порядка предназначен для применения в искусственный интеллект и программная инженерия, разработанная в SRI International.

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

SNARK используется как компонент рассуждений в НАСА Проект интеллектуальных систем. Это написано в Common Lisp и доступен под Общественная лицензия Mozilla.

Смотрите также

Рекомендации

  • М. Штикель, Р. Вальдингер, М. Лоури, Т. Прессбургер и И. Андервуд. «Дедуктивная композиция астрономического программного обеспечения из библиотек подпрограмм». Материалы Двенадцатой Международной конференции по автоматизированному дедуктивному переводу (CADE-12), Нанси, Франция, июнь 1994 г., страницы 341–355.
  • Ричард Уолдингер, Мартин Редди и Дженнифер Дунган. "Дедуктивная композиция из нескольких источников данных. "Май 2002 г. Отчет о ходе выполнения исследовательской задачи по интеллектуальному пониманию данных, проект интеллектуальной системы, НАСА SISM.
  • Р., Вальдингер, D. E. Appelt, J. Fry, D. J. Israel, P. Jarvis, D. Martin, S. Riehemann, M. E. Stickel, M. Tyson, J. Hobbs и J. L. Dungan. "Дедуктивный ответ на вопрос из нескольких ресурсов. " в Новые направления в ответах на вопросы, AAAI, 2004.
  • Р. Вальдингер, П. Джарвис и Дж. Дунган. «Использование дедукции для хореографии нескольких источников данных». В Семантические веб-технологии для поиска и извлечения, Остров Санибел, Флорида, октябрь 2003 г.

внешняя ссылка