Presenting machine-found proofs

DOI10.1007/3-540-61511-3_83MaRDI QIDQ4647515zbMATH OpenOpenAlexFDO

Authors Xiaorong Huang, Armin Fiedler

Publication date 15 January 2019

Published in Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL http://nbn-resolving.de/urn/resolver.pl?urn:nbn:de:hbz:386-kluedo-2086

zbMATH Keywords

intermediate representationlinguistic resourcemathematical textbooknatural deductionresolution proof

Mathematics Subject Classification ID

Recommendations

• Machine-assisted proofs
• scientific article; zbMATH DE number 1024410
• Toward mechanical methods for streamlining proofs
• scientific article; zbMATH DE number 4164180
• scientific article; zbMATH DE number 2102718
• The machinery of consistency proofs
• Revitalized automatic proofs: demonstrations
• The use of machines to assist in rigorous proof
• scientific article; zbMATH DE number 1136108

Cites work

• scientific article; zbMATH DE number 4164180 (Why is no real title available?)
• scientific article; zbMATH DE number 3684929 (Why is no real title available?)
• Reconstructing proofs at the assertion level
• The translation of formal proofs into English
• Untersuchungen über das logische Schliessen. I

Cited in

(11)

• Presenting inequations in mathematical proofs
• scientific article; zbMATH DE number 1614717 (Why is no real title available?)
• Assertion-level proof representation with under-specification
• scientific article; zbMATH DE number 2185656 (Why is no real title available?)
• PROVERB
• scientific article; zbMATH DE number 1104364 (Why is no real title available?)
• scientific article; zbMATH DE number 1140678 (Why is no real title available?)
• Reconstructing proofs at the assertion level
• \(\Omega\)\textsc{mega}: towards a mathematical assistant
• Mechanizing Mathematical Reasoning
• MBase: Representing knowledge and context for the integration of mathematical software systems

Describes a project that uses

Uses Software

• Omega-MKRP

This page was built for publication: Presenting machine-found proofs

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