Model-theoretic conservative extension for definitional theories
From MaRDI portal
Publication:2333319
DOI10.1016/j.entcs.2018.10.009zbMath1434.03028OpenAlexW2898891135WikidataQ113317506 ScholiaQ113317506MaRDI QIDQ2333319
Publication date: 12 November 2019
Full work available at URL: https://doi.org/10.1016/j.entcs.2018.10.009
Isabelleclassical higher-order logicconservative theory extensiondefinitional theoriesground semanticsmodel-theoretic conservativity
Mechanization of proofs and logical operations (03B35) Basic properties of first-order languages and structures (03C07) Higher-order logic (03B16) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Uses Software
Cites Work
- Unnamed Item
- On definitions of constants and types in HOL
- Isabelle/HOL. A proof assistant for higher-order logic
- An introduction to mathematical logic and type theory: To truth through proof.
- HOL with Definitions: Semantics, Soundness, and a Verified Implementation
- HOL Constant Definition Done Right
- A Consistent Foundation for Isabelle/HOL
- Comprehending Isabelle/HOL’s Consistency
- Checking Conservativity of Overloaded Definitions in Higher-Order Logic
This page was built for publication: Model-theoretic conservative extension for definitional theories