MUSCADET

MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics 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.