Automated Generation of Interesting Theorems

In the logical theory of a set of axioms there are many boring 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 domain. 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 ranking to identify interesting theorems among the logical consequences.

• Type: Conference
• Year: 2006
• Where: FLAIRS
• Authors: Yury Puzis, Yi Gao, Geoff Sutcliffe
• Keywords: Artificial Intelligence, Boring Logical Consequences, FLAIRS 2006, Interesting Ones, Logical Consequences