On definitions of constants and types in HOL

DOI10.1007/s10817-016-9366-4zbMath1356.68173OpenAlexW2294931363WikidataQ59476343 ScholiaQ59476343MaRDI QIDQ287358

Rob Arthan

Publication date: 26 May 2016

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

Full work available at URL: https://doi.org/10.1007/s10817-016-9366-4

zbMATH Keywords

higher-order logicconservative extensioninteractive theorem proving

Mathematics Subject Classification ID

Related Items

ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ Comprehending Isabelle/HOL’s Consistency ⋮ From LCF to Isabelle/HOL ⋮ Model-theoretic conservative extension for definitional theories

Uses Software

• Isabelle
• Isabelle/Isar
• Isar
• HOL
• ProofPower
• HOL Light
• HOL-Omega
• Z
• HOL Zero
• OpenTheory

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Z
• Structured theory development for a mechanized logic
• 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
• HOL with Definitions: Semantics, Soundness, and a Verified Implementation
• HOL Constant Definition Done Right
• HOL Light: An Overview
• The HOL-Omega Logic
• A Brief Overview of HOL4
• Towards Self-verification of HOL Light
• Axiom of Choice and Complementation
• Completeness in the theory of types