SNARK (New Automated Reasoning Kit от SRI) — это средство для доказательства теорем для многосортной логики первого порядка, предназначенное для приложений в области искусственного интеллекта и разработки программного обеспечения , разработанное в SRI International .
Основными механизмами вывода SNARK являются разрешение и парамодуляция ; кроме того, он предлагает специализированные процедуры принятия решений для конкретных областей, например, решатель ограничений для логики временных интервалов Аллена. В отличие от многих других средств доказательства теорем полностью автоматизирован (неинтерактивный). SNARK предлагает множество стратегических элементов управления для настройки своего поведения при поиске и, таким образом, настройки его производительности для конкретных приложений. Это, вместе с использованием многосортной логики и средств для интеграции специальных процедур рассуждений с универсальным выводом, делает его особенно подходящим для рассуждений для больших наборов утверждений.
SNARK используется в качестве компонента рассуждений в проекте NASA Intelligent Systems Project . Он написан на Common Lisp и доступен под лицензией Mozilla Public License .