SNARK, (el nuevo kit de razonamiento automatizado de SRI) , es un probador de teoremas para la lógica de primer orden de múltiples ordenamientos destinados 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á completamente 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 de múltiples ordenamientos y las facilidades para integrar procedimientos de razonamiento de propósito especial con 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 disponible bajo la licencia pública de Mozilla .
Ver también
Referencias
- M. Stickel, R. Waldinger , M. Lowry, T. Pressburger e I. Underwood. "Composición deductiva de software astronómico de bibliotecas de subrutinas". Actas de la Duodécima Conferencia Internacional sobre Deducción Automatizada (CADE-12) , Nancy, Francia, junio de 1994, páginas 341–355.
- Richard Waldinger , Martin Reddy y Jennifer Dungan. " Composición deductiva de múltiples fuentes de datos " . Informe de progreso de mayo de 2002 de la tarea de investigación sobre comprensión de datos inteligentes, Proyecto de sistema inteligente, NASA SISM.
- R, Waldinger , DE Appelt, J. Fry, DJ Israel, P. Jarvis, D. Martin, S. Riehemann, ME Stickel, M. Tyson, J. Hobbs y JL Dungan. " Respuesta deductiva a preguntas de varios recursos ", en Nuevas direcciones en la respuesta a preguntas , AAAI , 2004.
- R. Waldinger , P. Jarvis y J. Dungan. "Uso de la deducción para coreografiar múltiples fuentes de datos". En Tecnologías de Web Semántica para Búsqueda y Recuperación , Sanibel Island, Florida, octubre de 2003.