Automated and Human Proofs in General Mathematics: An Initial Comparison

DOI10.1007/978-3-642-28717-6_6zbMath1352.68211OpenAlexW2399825514MaRDI QIDQ2891438

Daniel Kühlwein, Josef Urban, Jesse Alama

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

Related Items (8)

MizAR 40 for Mizar 40 ⋮ SEPIA: Search for Proofs Using Inferred Automata ⋮ A learning-based fact selector for Isabelle/HOL ⋮ Learning-assisted theorem proving with millions of lemmas ⋮ Theorem Proving in Large Formal Mathematics as an Emerging AI Field ⋮ Machine learning guidance for connection tableaux ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\) ⋮ Premise selection for mathematics by corpus analysis and kernel methods

Uses Software

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

This page was built for publication: Automated and Human Proofs in General Mathematics: An Initial Comparison