We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Mechanisation of Model-theoretic Conservative Extension for HOL with Ad-hoc Overloading

Abstract: 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 Isabelle/HOL, definable symbols are types and constants. The latter may be ad-hoc overloaded, i.e. have different definitions for non-overlapping types. We prove that symbols that are independent of a new definition may keep their interpretation in a model extension. This work revises our earlier notion of model-theoretic conservative extension and generalises an earlier model construction. We obtain consistency of theories of definitions in higher-order logic (HOL) with ad-hoc overloading as a corollary. Our results are mechanised in the HOL4 theorem prover.
Comments: In Proceedings LFMTP 2020, arXiv:2101.02835
Subjects: Logic in Computer Science (cs.LO)
ACM classes: F.3.1; F.3.2
Journal reference: EPTCS 332, 2021, pp. 1-17
DOI: 10.4204/EPTCS.332.1
Cite as: arXiv:2101.03807 [cs.LO]
  (or arXiv:2101.03807v1 [cs.LO] for this version)

Submission history

From: EPTCS [view email]
[v1] Mon, 11 Jan 2021 10:51:17 GMT (28kb)

Link back to: arXiv, form interface, contact.