A Mizar mode for HOL

DOI10.1007/BFB0105406MaRDI QIDQ6567713zbMATH OpenFDO

Authors John R. Harrison

Publication date 5 July 2024

Full work available at URL https://doi.org/10.1007/BFB0105406

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• scientific article; zbMATH DE number 1863397
• A comparison of Mizar and Isar
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Twenty Years of Theorem Proving for HOLs Past, Present and Future
• scientific article; zbMATH DE number 2090293

Cites work

• A deficiency of natural deduction
• A higher-order implementation of rewriting
• A Prolog technology theorem prover: Implementation by an extended Prolog compiler
• A unification algorithm for typed \(\bar\lambda\)-calculus
• An examination of the prolog technology theorem-prover
• Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
• Edinburgh LCF. A mechanized logic of computation
• Formalizing a Hierarchical Structure of Practical Mathematical Reasoning
• scientific article; zbMATH DE number 2185681 (Why is no real title available?)
• scientific article; zbMATH DE number 3907807 (Why is no real title available?)
• scientific article; zbMATH DE number 234014 (Why is no real title available?)
• scientific article; zbMATH DE number 3351217 (Why is no real title available?)
• Isabelle. A generic theorem prover
• lean\(T^ AP\): Lean tableau-based deduction
• Minimizing the number of clauses by renaming
• Obvious inferences
• On the shape of mathematical arguments
• Optimizing proof search in model elimination
• Set theory in first-order logic: Clauses for Gödel's axioms

This page was built for publication: A Mizar mode for HOL

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