SNARK, (Nuevo Kit de Razonamiento Automatizado de SRI) , es un probador de teoremas para lógica de primer orden de clasificación múltiple destinado a aplicaciones en inteligencia artificial e ingeniería de software , desarrollado en SRI International .
Los principales mecanismos de inferencia de SNARK son la resolución y la paramodulación ; además, ofrece procedimientos de decisión especializados para dominios particulares, por ejemplo, un solucionador de restricciones para la lógica de intervalo temporal de Allen. A diferencia de muchos otros probadores de teoremas, está totalmente automatizado (no interactivo). SNARK ofrece muchos controles estratégicos para ajustar su comportamiento de búsqueda y así ajustar su rendimiento a aplicaciones particulares. Esto, junto con el uso de la lógica multiordenada y las facilidades para integrar los procedimientos de razonamiento de propósito especial con la inferencia de propósito general, lo hacen particularmente adecuado como razonador para grandes conjuntos de afirmaciones.
SNARK se utiliza como componente de razonamiento en el Proyecto de Sistemas Inteligentes de la NASA . Está escrito en Common Lisp y está disponible bajo la Licencia Pública de Mozilla .