CASE Project

Team:

• Cordell Green (PI)
• Stephen Westfold (Co-PI)
• Alessandro Coglio
• Christoph Kreitz
• Eric Smith

This project is part of the DARPA CASE program. Our goal is to improve the scalability and explainability of formal inference tools like theorem provers and constraint solvers. Our approach is to build Flex, a resolution theorem prover that may include constraint solvers, by (1) writing a high-level formal specification and (2) applying sequences of automated, proof-producing transformations to generate implementations. By incorporating domain knowledge into the specification and transformation process, we will generate domain-specialized implementations of Flex that will scale better than general-purpose provers and solvers in the domains of specialization. The incorporation of domain knowledge will also enable the generation of Flex implementations that provide higher-level, domain-specific explanations of both successful and unsuccessful inferences.