Automated theorem proving

Deliver an automated reasoning system, as an extension to Vampire/Deepire, that can reason over the CoreSense HOL ontology and is optimized for it. This will include machine learning extensions and optimized strategies for higher-order Vampire, as well as extensions for reasoning with the closed world assumption and various modal logic and temporal logic operators.