3 Result(s)
-
Article
Open AccessDouble Negation Semantics for Generalisations of Heyting Algebras
This paper presents an algebraic framework for investigating proposed translations of classical logic into intuitionistic logic, such as the four negative translations introduced by Kolmogorov, Gödel, Gentzen ...
-
Article
Open AccessSelf-Formalisation of Higher-Order Logic
We present a mechanised semantics for higher-order logic (HOL), and a proof of soundness for the inference system, including the rules for making definitions, implemented by the kernel of the HOL Light theorem...
-
Article
Open AccessOn Definitions of Constants and Types in HOL
This paper reports on a simpler and more powerful replacement for the principles for defining new constants that were previously provided in the various HOL implementations. We discuss the problems that the ne...
