Abstract

Automated theorem finding (ATF), originally advocated by Larry T. Wos as a research direction distinct from automated theorem proving (ATP), aims at discovering previously unknown theorems rather than proving a given conjecture. While the distinction between theorem finding and theorem proving was clearly recognized in the late 1980s, a fundamental question remained largely unexplored: What underlying logic system as the logical foundation is most appropriate for automated theorem finding? Beginning in 1994, Jingde Cheng initiated a long-term research program addressing this question and expanding the wide application of automated theorem finding. Challenging the prevailing assumption that classical mathematical logic is an adequate foundation for all forms of automated reasoning, Cheng argued that the essential characteristics of theorem finding are fundamentally different from those of theorem proving. In particular, due to the large number of implication paradoxes in classical mathematical logic, a massive amount of “garbage theorems” are generated during forward reasoning based on classical mathematical logic, making it fundamentally unsuitable for discovery-oriented reasoning. To overcome the limitations of classical mathematical logic, Cheng proposed a strong relevant logic approach to automated theorem finding and subsequently developed a comprehensive framework based on strong relevant logic including entailment calculus, forward deduction engines, relevant reasoning, predicate abstraction and suggestion, and theorem-interestingness measurement. Over the next two decades, this framework has gradually evolved into a systematic methodology, encompassing entailment calculus based on strong relevant logic, general-purpose forward deduction engines, parallel forward reasoning, relevant (deductive, inductive, abductive) reasoning, automated theorem finding in mathematics, predicate abstraction and suggestion algorithms, theorem-interestingness measurement, theory grid and distributed cooperative discovery, semi-lattice models of formal theories, epistemic operations, epistemic programming paradigm, knowledge appreciation, and general methodology for automatic discovery and prediction. This paper reviews the entire development process of this research program and points out that its most significant principal originality lies in establishing, for the first time in the world, a method for discovery-oriented reasoning supported by strong relevant logic as the underlying logical system. The core conclusion of this research program is that while classical mathematical logic provides a suitable logical foundation for theorem proving, it cannot support theorem finding at all, while strong relevant logic provides a more suitable logical foundation for discovery-oriented reasoning and automated scientific discovery. The ultimate goal of this research program is to achieve automated scientific discovery and automated scientific prediction with human as the agent.