A formalization and proof checker for Isabelle's metalogic

DOI10.1007/S10817-022-09648-WzbMATH Open1502.68353OpenAlexW4312126060MaRDI QIDQ2108191FDOQ2108191

Authors Simon Roßkopf, Tobias Nipkow

Publication date 19 December 2022

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-022-09648-w

zbMATH Keywords

theorem provinghigher-order logicIsabellemetalogicproof checker

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Formalization of mathematics in connection with theorem provers (68V20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• The foundation of a generic theorem prover
• The Isabelle Framework
• scientific article; zbMATH DE number 1088221
• A verified proof checker for higher-order logic
• Isabelle/HOL. A proof assistant for higher-order logic

Cites work

• scientific article; zbMATH DE number 1670734 (Why is no real title available?)
• scientific article; zbMATH DE number 4180832 (Why is no real title available?)
• scientific article; zbMATH DE number 1301729 (Why is no real title available?)
• scientific article; zbMATH DE number 482967 (Why is no real title available?)
• scientific article; zbMATH DE number 2085164 (Why is no real title available?)
• A consistent foundation for Isabelle/HOL
• A consistent foundation for Isabelle/HOL
• A formalized general theory of syntax with bindings: extended version
• A verified proof checker for higher-order logic
• CakeML
• Code generation via higher-order rewrite systems
• Comprehending Isabelle/HOL’s Consistency
• Concrete semantics. With Isabelle/HOL
• Constructive Type Classes in Isabelle
• Data refinement in Isabelle/HOL
• HOL Zero's solutions for Pollack-inconsistency
• Isabelle's metalogic: formalization and proof checker
• Isabelle. A generic theorem prover
• Isabelle/HOL. A proof assistant for higher-order logic
• Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
• Light-weight containers for Isabelle: efficient, extensible, nestable
• Metamath Zero: designing a theorem prover prover
• More Church-Rosser proofs (in Isabelle/HOL)
• Nominal techniques in Isabelle/HOL
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Sets in Coq, Coq in Sets
• Seventy-five problems for testing automatic theorem provers
• The Isabelle collections framework
• The foundation of a generic theorem prover
• The reflective Milawa theorem prover is sound (down to the machine code that runs it)
• Towards Self-verification of HOL Light
• Type Reconstruction for Type Classes

Cited in

(5)

• The foundation of a generic theorem prover
• Isabelle's metalogic: formalization and proof checker
• Eisbach: a proof method language for Isabelle
• αCheck: A mechanized metatheory model checker
• A verified proof checker for higher-order logic

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Twelf
• CakeML
• Milawa
• Nominal Isabelle
• Jitawa
• HOL Zero
• Transfer
• Lifting
• Elf
• OpenTheory
• Metamath Zero

This page was built for publication: A formalization and proof checker for Isabelle's metalogic

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