MUSCADET 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 Standard Articles 3 Publications describing the Software, including 3 Publications in zbMATH Year Strong and weak points of the MUSCADET theorem prover – examples from CASC-JC. Zbl 1019.68102Pastre, Dominique 2002 MUSCADET 2. 3: A knowledge-based theorem prover based on natural deduction. Zbl 0988.68594Pastre, Dominique 2001 MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics. Zbl 0668.68103Pastre, Dominique 1989 all top 5 Cited by 10 Authors 4 Pastre, Dominique 1 Ferrari, Mauro 1 Fiorentini, Camillo 1 Goré, Rajeev Prabhakar 1 Leitsch, Alexander 1 Li, Dafa 1 McMichael, A. F. 1 Nipkow, Tobias 1 Sieg, Wilfried 1 Walsh, Patrick M. all top 5 Cited in 6 Serials 1 Artificial Intelligence 1 Journal of Automated Reasoning 1 AI Communications 1 Annals of Mathematics and Artificial Intelligence 1 Lecture Notes in Computer Science 1 The Review of Symbolic Logic Cited in 3 Fields 9 Computer science (68-XX) 3 Mathematical logic and foundations (03-XX) 1 General and overarching topics; collections (00-XX) Citations by Year