Tsuyoshi Murata, Masamichi Shimura
In the discovery of useful theorems or formulas, experimental data acquisition plays a fundamental role. Most of the previous discovery systems which have the abilities for experimentation, however, require much knowledge for evaluating experimental results, or require plans of common experiments which are given to the systems in advance. Only few systems have been attempted to make experiments which enable the discovery based on acquired experimental data without depending on given initial knowledge. This paper proposes a new approach for discovering useful theorems in the domain of plane geometry by employing experimentation. In this domain, drawing a figure and observing it correspond to making experimentation since these two processes are preparations for acquiring geometrical data. EXPEDITION, a discovery system based on experimental data acquisition, generates figures by itself and acquires expressions describing relations among line segments and angles in the figures. Such expressions can be extracted from the numerical data obtained in the computer experiments. By using simple heuristics for drawing and observing figures, the system succeeds in discovering many new useful theorems and formulas as well as rediscovering well-known theorems, such as power theorems and Thales’ theorem.