MPTP 0.1 -- system description

DOI10.1016/S1571-0661(04)80659-5MaRDI QIDQ4916228zbMATH OpenFDO

Authors Josef Urban

Publication date 19 April 2013

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S1571-0661(04)80659-5

Mathematics Subject Classification ID

Recommendations

• MPTP-motivation, implementation, first experiments
• MPTP 0.2: Design, implementation, and initial experiments
• The TPTP problem library
• scientific article; zbMATH DE number 1951640
• ATP Cross-Verification of the Mizar MPTP Challenge Problems

Cites work

• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• scientific article; zbMATH DE number 1507187 (Why is no real title available?)
• Soft typing for ordered resolution
• The TPTP problem library. CNF release v1. 2. 1

Cited in

(8)

• Translating the IMPS theory library to MMT/OMDoc
• scientific article; zbMATH DE number 1614711 (Why is no real title available?)
• System description: GAPT 2.0
• SMTtoTPTP -- a converter for theorem proving formats
• ATP Cross-Verification of the Mizar MPTP Challenge Problems
• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• MPTP-motivation, implementation, first experiments
• MPTP 0.2: Design, implementation, and initial experiments

Describes a project that uses

Uses Software

• Mizar
• SPASS
• TPTP
• MPTP
• MML

This page was built for publication: MPTP 0.1 -- system description

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