On definitions of constants and types in HOL
From MaRDI portal
Publication:287358
DOI10.1007/S10817-016-9366-4zbMATH Open1356.68173DBLPjournals/jar/Arthan16OpenAlexW2294931363WikidataQ59476343 ScholiaQ59476343MaRDI QIDQ287358FDOQ287358
Authors: 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
Recommendations
Cites Work
- The HOL-Omega Logic
- A Brief Overview of HOL4
- Z
- Title not available (Why is that?)
- 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
- Towards Self-verification of HOL Light
- Title not available (Why is that?)
- Axiom of Choice and Complementation
- Interactive theorem proving from the perspective of Isabelle/Isar
- Completeness in the theory of types
Cited In (9)
- From types to sets by local type definition in higher-order logic
- From types to sets by local type definitions in higher-order logic
- Model-theoretic conservative extension for definitional theories
- On the two definitions of Ho(pro C)
- ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT
- Stateless HOL
- From LCF to Isabelle/HOL
- A consistent foundation for Isabelle/HOL
- Comprehending Isabelle/HOL’s Consistency
Uses Software
This page was built for publication: On definitions of constants and types in HOL
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q287358)
