MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics (Q1118426)

The author presents a somewhat informal description of a heuristic theorem prover conceived as an expert system using a modular knowledge base expressed in a user-friedly language. \(\{\) More detailed information seems to be available in the author's thèse d'état (Un système de démonstration automatique de théorèmes utilisant connaissances et métaconnaissances en mathématique Université Paris VI, 1984).\(\}\) The inference part of MUSCADET is based on natural reduction, the knowledge base is adapted to prove theorems in point-set topology and topological linear spaces. The main ideas are exemplified by automatic proofs of some elementary facts on topological linear spaces. \{The author claims to have consulted ``high-level mathematicians'', but their reported performance when exposed to simple problems which every student after a first week in a course on topological vector spaces could solve after a moment's reflection seems rather poor.\}