On Combining Automated Theorem Proving and Digital Engineering for General Intelligence

In recent years, engineering intelligent systems has become closely related to integrating artificial intelligence (AI) or machine learning (ML) components into systems. There is a general sense that as the availability of computational resources scales, the intelligence of AI and ML components will scale, thus scaling the intelligence of the system as a whole. While this bottom-up approach has merit, it takes the task of engineering intelligence out of the hands of systems engineers and gives it to AI and ML engineers. In this paper, an alternative approach to engineering intelligence is outlined based on combining the concepts of automated theorem proving (ATP) and digital engineering. Instead of using AI and ML at the component-level, ATP can be applied at the systems-level to digital models and environments. By systematically solving proofs related to properties, functional requirements, and performance, ATP can contribute to the design, operation, and regulation of intelligent systems. This paper substantiates the use of ATP in digital engineering by using model-based systems engineering as an interface between the two. This paper illustrates this interface with a descriptive example in unmanned aerial systems. Ultimately, the use of ATP with digital engineering provides a top-down, systems-centric alternative to using AI and ML components as the primary means of engineering intelligence.