Zobrazeno 1 - 4
of 4
pro vyhledávání: '"Gengelbach, Arve"'
Publikováno v:
EPTCS 332, 2021, pp. 1-17
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 ma
Externí odkaz:
http://arxiv.org/abs/2101.03807
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. In this paper, we present a mechanised proof that HOL with ad-hoc overl
Externí odkaz:
http://arxiv.org/abs/2002.10212
Non-terminating (dependencies of) definitions can lead to logical contradictions, for example when defining a boolean constant as its own negation. Some proof assistants thus detect and disallow non-terminating definitions. Termination is generally u
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::1726c08a47a87c1140fc2915702b143c
Autor:
Gengelbach, Arve
With an ever growing dependency on computer systems, the need to guarantee their correct behaviour increases. Mathematically rigorous techniques like formal verification offer a way to derive a system's mathematical properties for example with the he
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::2c82e9a92eb1bfcec8ada128e0e0e700
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-435841
http://urn.kb.se/resolve?urn=urn:nbn:se:uu:diva-435841