Translating Mizar for first order theorem provers

DOI10.1007/3-540-36469-2_16MaRDI QIDQ4413895zbMATH OpenFDO

Authors Josef Urban

Publication date 21 July 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2594/25940203.htm

Mathematics Subject Classification ID

Knowledge representation (68T30)

Recommendations

• MPTP-motivation, implementation, first experiments
• Interpretation of a Mizar-like logic in first order logic
• ATP-based cross-verification of Mizar proofs: method, systems, and first experiments
• MPTP 0.1 -- system description
• The Mizar Mathematical Library in OMDoc: translation and applications

Cited in

(21)

• System description: XSL-based translator of Mizar to {\LaTeX}
• On rewriting rules in Mizar
• Experiences from exporting major proof assistant libraries
• A new export of the Mizar mathematical library
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Extracting Higher-Order Goals from the Mizar Mathematical Library
• Enhancement of \textsc{Mizar} texts with transitivity property of predicates
• MizAR 40 for Mizar 40
• Definitional expansions in Mizar. In memoriam of Andrzej Trybulec, a pioneer of computerized formalization
• Translating a Dependently-Typed Logic to First-Order Logic
• Interpretation of a Mizar-like logic in first order logic
• Theorem proving in large formal mathematics as an emerging AI field
• MPTP 0.1 -- system description
• On the Structure of Mizar Types
• Licensing the Mizar Mathematical Library (MML)
• MPTP-motivation, implementation, first experiments
• Translating SUMO-K to Higher-Order Set Theory
• Hammering higher order set theory
• Machine learning for quantifier selection in cvc5
• Learning guided automated reasoning: a brief survey
• MPTP 0.2: Design, implementation, and initial experiments

Describes a project that uses

Uses Software

• SPASS
• Mizar

This page was built for publication: Translating Mizar for first order theorem provers

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