Proof-theoretic conservative extension of HOL with ad-hoc overloading

DOI10.1007/978-3-030-64276-1_2OpenAlexW3110490929MaRDI QIDQ2037933

Arve Gengelbach, Tjark Weber

Publication date: 8 July 2021

Full work available at URL: https://doi.org/10.1007/978-3-030-64276-1_2

zbMATH Keywords

Isabelleclassical higher-order logicad-hoc overloadingconservative theory extensionproof-theoretic conservativity

Mathematics Subject Classification ID

Theory of computing (68Qxx)

Uses Software

• Isabelle/HOL

This page was built for publication: Proof-theoretic conservative extension of HOL with ad-hoc overloading