Extracting Higher-Order Goals from the Mizar Mathematical Library

DOI10.1007/978-3-319-42547-4_8zbMath1344.68203arXiv1605.06996OpenAlexW2401700265MaRDI QIDQ2817297

Josef Urban, Chad Edward Brown

Publication date: 30 August 2016

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1605.06996

zbMATH Keywords

higher-order logicset theoryautomated theorem provingformalized mathematics

Mathematics Subject Classification ID

Related Items (1)

Semantics of Mizar as an Isabelle object logic

Uses Software

• LEO-II
• MPTP
• MPTP 0.2
• Mizar
• Satallax
• E Theorem Prover

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The higher-order prover \textsc{Leo}-II
• MPTP-motivation, implementation, first experiments
• MPTP 0.2: Design, implementation, and initial experiments
• Reducing higher-order theorem proving to a sequence of SAT problems
• A formulation of the simple theory of types

This page was built for publication: Extracting Higher-Order Goals from the Mizar Mathematical Library