-
Chapter
HOL
Statement
-
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 and Conference Paper
The 1st Verified Software Competition: Experience Report
We, the organizers and participants, report our experiences from the 1st Verified Software Competition, held in August 2010 in Edinburgh at the VSTTE 2010 conference.
-
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...
-
Article
A Hoare logic for linear systems
We consider reasoning about linear systems expressed as block diagrams that give a graphical representation of a system of differential equations or recurrence equations. We use the notion of additive relation...
-
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...
-
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
Studying Algebraic Structures Using Prover9 and Mace4
In this chapter we present a case study, drawn from our research work, on the application of a fully automated theorem prover together with an automatic counter-example generator in the investigation of a clas...
-
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 ...
