2 citations · 2 across the 1 of their papers we have counts for
2 papers
cs.LO2021★ 2 cited
Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading
Arve Gengelbach, Johannes Åman Pohjola, Tjark Weber
Definitions of new symbols merely abbreviate expressions in logical frameworks, and no new facts (regarding previously defined symbols) should hold because of a new definition. In…
cs.LO2020
A Mechanised Semantics for HOL with Ad-hoc Overloading
Johannes Åman Pohjola, Arve Gengelbach
Isabelle/HOL augments classical higher-order logic with ad-hoc overloading of constant definitions---that is, one constant may have several definitions for non-overlapping types. I…