ITR: Little Engines of Proof

计算机主要用于自动进行数值计算，但也可以通过编程来通过符号计算进行推理。强大的自动化推理是灵活可靠的计算基础设施的关键。这种技术可以用来建立和分析复杂系统的抽象模型，发现软件和硬件设计中的错误和优化，以及设计更具表现力的编程语言。参考技术的这些工程应用需要可嵌入和可组合的轻量级推理工具。该项目是SRI国际公司、克拉克森大学和佩斯大学共同努力的成果，旨在为推理软件组件构建一个开放的基础设施。推论！项目通过逻辑中间件层为一系列基本推理能力提供抽象接口。推论！中间件还包括不同理论和抽象层次之间的组合和映射机制。该课程的理论和教学基础！项目是在一门名为“推理分析”的学科中开发的，该学科研究有效的推理组件以及它们可以在其中组合的架构框架。推论！技术被用来探索新的和令人兴奋的应用，包括复杂现象的定性建模和高保证的开源软件。该项目通过将传统的单一推理框架分解成可以以开源形式交换并嵌入到开放验证技术中的有用组件来寻求在研究和教育中的广泛影响。该项目的一个关键部分是为核查和分析研究界内的组件开放交换建立标准和接口。这一努力包括与开放源码软件社区积极合作，开发可集成的验证组件，用于构建可靠的、经过验证的和自我检查的软件。

Computers are primarily used for automating numericalcalculation but they can also be programmed to make inferences throughsymbolic calculation. Powerful automated inference is key to a flexibleand reliable computing infrastructure. Such technology can be used tobuild and analyze abstract models of complex systems, find bugs andoptimizations in software and hardware designs, and in the design of moreexpressive programming languages. These engineering applications ofinference technology require lightweight inference tools that areembeddable and composable.The Infer! project is a collaborative effort between SRI International,Clarkson University, and Pace University to construct an open foundationalinfrastructure for inferential software components. The Infer! projectprovides an abstract interface to a range of basic inference capabilitiesthrough a logic middleware layer. The Infer! middleware also includesmechanisms for combining and mapping between different theories and levelsof abstraction. The theoretical and pedagogical foundations for theInfer! project are developed in a discipline called "inferential analysis"that studies efficient inference components and the architecturalframework within which they can be combined. The Infer! technology isused to explore novel and exciting applications including the qualitativemodeling of complex phenomena and high-assurance open-source software.Broader impacts in research and education are sought for this projectby decomposing traditionally monolithic inference frameworks into usefulcomponents that can be exchanged in open source form and embedded withinopen verification technology. A key part of the project is an outreacheffort to establish standards and interfaces for an open exchange ofcomponents within the verification and analysis research community. Thiseffort includes active cooperation with the open source software communitythrough the development of verification components that can be integratedfor use in constructing dependable, verified, and self-checking software.