Mechanizing Mathematical Reasoning

DOI10.1007/B106663MaRDI QIDQ5717445zbMATH OpenOpenAlexFDO

Authors Christoph Benzmüller, Andreas Meier, Volker Sorge

Publication date 10 January 2006

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/b106663

Mathematics Subject Classification ID

Information storage and retrieval of data (68P20) Knowledge representation (68T30)

Recommendations

• MPTP-motivation, implementation, first experiments
• scientific article; zbMATH DE number 1614716
• Automated theorem proving in mathematics.
• Knowledge-based proof planning
• Virtual theories -- a uniform interface to mathematical knowledge bases

Cited in

(4)

• MUSCADET: An automatic theorem proving system using knowledge and metaknowledge in mathematics
• Learning domain knowledge to improve theorem proving
• Publication/Citation: A Proof-Theoretic Approach to Mathematical Knowledge Management*
• Computer supported mathematics with MEGA

Describes a project that uses

Uses Software

• VAMPIRE
• SETHEO
• TPTP
• Mizar
• HOL
• MBase
• MathWeb
• PROSPER
• OMEGA
• PROTEIN
• TRAMP
• Mathematica
• TPS
• OTTER
• PVS
• Waldmeister
• Bliksem
• KOMET
• Medmaker
• SPASS
• Nuprl
• CLAM

This page was built for publication: Mechanizing Mathematical Reasoning

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5717445)