A formalization and proof checker for Isabelle's metalogic

DOI10.1007/S10817-022-09648-WMaRDI QIDQ2108191zbMATH OpenOpenAlexFDO

Authors Simon Roßkopf, Tobias Nipkow

Publication date 19 December 2022

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

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

higher-order logicIsabellemetalogicproof checkertheorem proving

Mathematics Subject Classification ID

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

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

• 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
• 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?)
• Isabelle. A generic theorem prover
• Isabelle's metalogic: formalization and proof checker
• 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 foundation of a generic theorem prover
• The Isabelle collections framework
• 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

(7)

• The foundation of a generic theorem prover
• A verified proof checker for higher-order logic
• Isabelle's metalogic: formalization and proof checker
• Eisbach: a proof method language for Isabelle
• scientific article; zbMATH DE number 1301858 (Why is no real title available?)
• αCheck: A mechanized metatheory model checker
• Exploiting instantiations from paramodulation proofs in Isabelle/HOL

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)