Automated and human proofs in general mathematics: an initial comparison

DOI10.1007/978-3-642-28717-6_6MaRDI QIDQ2891438zbMATH OpenOpenAlexFDO

Authors Jesse Alama, Daniel Kühlwein, Josef Urban

Publication date 15 June 2012

Published in Logic for Programming, Artificial Intelligence, and Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-642-28717-6_6

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• Evaluation of automated theorem proving on the Mizar mathematical library
• MPTP-motivation, implementation, first experiments
• MizAR 40 for Mizar 40
• scientific article; zbMATH DE number 1951639
• Theorem proving in large formal mathematics as an emerging AI field

Cited in

(14)

• Automated proofs of equality problems in Overbeek's competition
• Machine learning guidance for connection tableaux
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Premise selection for mathematics by corpus analysis and kernel methods
• MizAR 40 for Mizar 40
• Automated proof compression by invention of new definitions
• A learning-based fact selector for Isabelle/HOL
• SEPIA: search for proofs using inferred automata
• scientific article; zbMATH DE number 1951639 (Why is no real title available?)
• Learning-assisted theorem proving with millions of lemmas
• Toward a procedure for data mining proofs
• Theorem proving in large formal mathematics as an emerging AI field
• Evaluation of automated theorem proving on the Mizar mathematical library
• ProofLang: the language of arXiv proofs

Describes a project that uses

Uses Software

• MPTP 0.2
• Mizar
• Sledgehammer
• MaLeCoP
• E Theorem Prover
• MaLARea
• MML

This page was built for publication: Automated and human proofs in general mathematics: an initial comparison

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