This paper presents Octopus, an automated theorem-proving system that combines learning and parallel search. The learning technique involves proving a simpler version of a given theorem and then using what it has learned to prove the given theorem. As of January 2004 Octopus had successfully proved 43 of the 1.0-rated theorems of the TPTP Problem Library.
Keywords automated theorem proving - learning strategies - Octopus - parallel search - TPTP