Algorithm-Supported Mathematical Theory Exploration: A Personal View and Strategy

Abstract. We present a personal view and strategy for algorithm-supported mathematical theory exploration and draw some conclusions for the desirable functionality of future mathematical software systems. The main points of emphasis are: The use of schemes for bottom-up mathematical invention, the algorithmic generation of conjectures from failing proofs for top-down mathematical invention, and the possibility to program new reasoners within the logic on which the reasoners work (“meta-programming”). 1 A View of Algorithm-Supported Mathematical Theory Exploration Mathematical theories are collections of formulae in some formal logic language (e.g. predicate logic). Mathematical theory exploration proceeds by applying, under the guidance of a human user, various algorithmic reasoners for producing new formulae from given ones and aims at building up (large) mathematical knowledge bases in an efficient, reliable, well-structured, re-usable, and flexible way. Algorithm-supported math...

• Type: Conference
• Year: 2004
• Where: AISC
• Authors: Bruno Buchberger
• Keywords: AISC 2004, Algorithm-supported Mathematical Theory, Artificial Intelligence, Mathematical Invention, Mathematical Theory Exploration