Automated Generation of Interesting Theorems

Yury Puzis, Yi Gao, Geoff Sutcliffe

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.

Subjects: 3. Automated Reasoning; 15.9 Theorem Proving

Submitted: Feb 10, 2006

This page is copyrighted by AAAI. All rights reserved. Your use of this site constitutes acceptance of all of AAAI's terms and conditions and privacy policy.