Proof-Producing Reflection for HOL

DOI10.1007/978-3-319-22102-1_11zbMath1465.03052OpenAlexW2228920119MaRDI QIDQ2945631

Ramana Kumar, Benja Fallenstein

Publication date: 14 September 2015

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-22102-1_11

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Large cardinals (03E55) Higher-order logic (03B16) Formalization of mathematics in connection with theorem provers (68V20)

Related Items (2)

Comprehending Isabelle/HOL’s Consistency ⋮ Extensible and Efficient Automation Through Reflective Tactics

Uses Software

• Isabelle
• HOL
• HOL Light
• Milawa

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
• Interactive theorem proving. 5th international conference, ITP 2014, held as part of the Vienna summer of logic, VSL 2014, Vienna, Austria, July 14--17, 2014. Proceedings
• Proof-producing translation of higher-order logic into pure and stateful ML
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• The Reflective Milawa Theorem Prover Is Sound
• HOL Light: An Overview
• A Brief Overview of HOL4
• The Isabelle Framework
• The Four Colour Theorem: Engineering of a Formal Proof
• Towards Self-verification of HOL Light
• Transfinite Progressions: A Second Look at Completeness
• Ordinals in HOL: Transfinite Arithmetic up to (and Beyond) ω 1
• Transfinite recursive progressions of axiomatic theories

This page was built for publication: Proof-Producing Reflection for HOL