Automated Generation of Interesting Theorems
Yury Puzis, Yi Qin Gao, Geoff Sutcliffe · 2004
In the logical theory of a set of axioms there are many bor-ing logical consequences, and scattered among them there are a few interesting ones. The few interesting ones include those that are singled out as theorems by experts in the do-main. This paper describes the techniques, implementation, and results of an automated system that generates logical consequences of a set of axioms, and uses filters and rank-ing to identify interesting theorems among the logical conse-quences. 1.