scientific article; zbMATH DE number 1507187

MaRDI QIDQ4503907zbMATH OpenFDO

Authors Ingo Dahn

Publication date 14 May 2001

zbMATH Keywords

abstract model theoryfirst-order theorem provingtyped logicuntyped first-order logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Recommendations

• scientific article; zbMATH DE number 1951640
• MPTP-motivation, implementation, first experiments
• Evaluation of automated theorem proving on the Mizar mathematical library
• MPTP 0.2: Design, implementation, and initial experiments
• Extracting Higher-Order Goals from the Mizar Mathematical Library

Cited in

(10)

• Semantics of Mizar as an Isabelle object logic
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Encoding monomorphic and polymorphic types
• Basic first-order model theory in Mizar
• scientific article; zbMATH DE number 1951640 (Why is no real title available?)
• MPTP 0.1 -- system description
• MPTP-motivation, implementation, first experiments
• Solving hard Mizar problems with instantiation and strategy invention
• Hammering higher order set theory
• MPTP 0.2: Design, implementation, and initial experiments

Describes a project that uses

Uses Software

• Mizar

This page was built for publication:

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