-
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...
-
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
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 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
