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

DOI10.1016/0004-3702(89)90035-0zbMath0668.68103OpenAlexW1986156613MaRDI QIDQ1118426

Dominique Pastre

Publication date: 1989

Published in: Artificial Intelligence (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0004-3702(89)90035-0

zbMATH Keywords

natural deductionexpert systemknowledge basetopological linear spacesautomatic proofsheuristic theorem provernatural reduction

Mathematics Subject Classification ID

Related Items

Automated theorem proving in mathematics. ⋮ MUSCADET

Uses Software

• REDUCE
• MACSYMA

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• An experimental logic based on the fundamental deduction principle
• Non-resolution theorem proving
• Doing arithmetic without diagrams
• Automatic theorem proving in set theory
• A language and a program for stating and solving combinatorial problems
• Towards the automation of set theory and its logic
• Observation du mathématicien: Aide à l'enseignement et à la demonstration automatique de théoremes
• A man-machine theorem-proving system
• An examination of the geometry theorem machine
• Splitting and reduction heuristics in automatic theorem proving
• Computer proofs of limit theorems
• Experiment with an automatic theorem-prover having partial ordering inference rules
• Automatic Proofs of Theorems in Analysis Using Nonstandard Techniques
• A Proof Procedure Using Connection Graphs
• A Machine-Oriented Logic Based on the Resolution Principle
• Algebraic simplification
• Symbolic integration