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.