swMATH ID: 6859
Software Authors: Pastre, Dominique
Description: 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.
Homepage: http://www.sciencedirect.com/science/article/pii/0004370289900350
Keywords: natural deduction; heuristic theorem prover; expert system; knowledge base; natural reduction; automatic proofs; topological linear spaces
Related Software: OTTER; Automath; Isabelle/ZF; MACSYMA; REDUCE; Nuprl; TPTP; VAMPIRE; P.rex; MODPROF; QUBE; E Theorem Prover; JProver; Racer; LoTREC; NoMoRe; SCOTT; DCTP; STRIP; lolliCoP
Cited in: 9 Publications

Citations by Year