ATP Cross-Verification of the Mizar MPTP Challenge Problems

DOI10.1007/978-3-540-75560-9_39MaRDI QIDQ3498492zbMATH OpenOpenAlexFDO

Authors Josef Urban, Geoff Sutcliffe

Publication date 15 May 2008

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-540-75560-9_39

Mathematics Subject Classification ID

Recommendations

• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• ATP and presentation service for Mizar formalizations
• MPTP 0.2: Design, implementation, and initial experiments
• MPTP-motivation, implementation, first experiments
• MPTP 0.1 -- system description

Cited in

(3)

• Theorem proving in large formal mathematics as an emerging AI field
• MPTP 0.1 -- system description
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments

Describes a project that uses

Uses Software

• MPTP
• MPTP 0.2
• VAMPIRE
• SPASS
• TPTP
• Isar
• Mizar
• E Theorem Prover
• MaLARea
• Ivy

This page was built for publication: ATP Cross-Verification of the Mizar MPTP Challenge Problems

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