A Bridge Between Rich Semantic Reasoning and Theorem Provers

In the history of the Cyc project, Cyc’s knowledge base and inference engine have evolved in a direction far different from most other automated theorem provers. Cyc concentrated on solving problems in very large knowledge spaces (i.e., millions of facts), using higher-order logic, although the problem solutions were often not very deep. The automated theorem proving community, on the other hand, looked at relatively small knowledge spaces (or theorems), but focused on becoming very fast at finding very deep solutions.

To date, there has been fairly little cross-pollination between the two communities. In part, this has been because there was no corpus of problems accessible by both Cyc and automated theorem provers. Now, however, just such a problem corpus has been released and made available in the TPTP (Thousands of Problems for Theorem Provers) format that is the standard for automated theorem proving researchers. More information about this problem suite can be found at


Leave a Reply

You must be logged in to post a comment.