![Loading...](https://link.springer.com/static/c4a417b97a76cc2980e3c25e2271af3129e08bbe/images/pdf-preview/spacer.gif)
-
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...
-
Chapter and Conference Paper
HOL Constant Definition Done Right
This note gives a proposal for a simpler and more powerful replacement for the mechanisms currently provided in the various HOL implementations for defining new constants.
-
Chapter and Conference Paper
HOL with Definitions: Semantics, Soundness, and a Verified Implementation
We present a mechanised semantics and soundness proof for the HOL Light kernel including its definitional principles, extending Harrison’s verification of the kernel without definitions. Soundness of the logic...
-
Chapter
(Dual) Hoops Have Unique Halving
Continuous logic extends the multi-valued Łukasiewicz logic by adding a halving operator on propositions. This extension is designed to give a more satisfactory model theory for continuous structures. The sema...
-
Chapter and Conference Paper
Computational Logic and Continuous Mathematics, Pure and Applied
Continuous problem domains are of ever-increasing importance in the application of computational logic to problems in systems engineering and to problems in mathematics and theoretical computer science. I will...
-
Chapter
HOL
Statement