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.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element