Interactive Theorem Proving

Asad Ahmed, Osman Hasan, Falah Awwad, Nabil Bastaki

Research output: Chapter in Book/Report/Conference proceedingChapter


Traditional analysis techniques cannot ascertain an accurate analysis for the safety- and mission-critical applications of smart grids due to their inability to exhaustively specify and verify the systems. To overcome these issues, we propose the theorem proving based methodology for an accurate analysis of smart grid problems which can be modeled using stability, microeconomics and algorithm design theories. We choose the HOL Light theorem prover to develop the proposed formalizations due to the availability of foundational theories, such as set, differential, real and complex, in the HOL Light library. In this chapter, we present a brief overview of the HOL Light theorem prover and commonly used formalizations from the HOL Light library to facilitate the understanding of the proposed formalizations which are presented, in the rest of the book.

Original languageEnglish
Title of host publicationSpringerBriefs in Applied Sciences and Technology
PublisherSpringer Science and Business Media Deutschland GmbH
Number of pages7
Publication statusPublished - 2022

Publication series

NameSpringerBriefs in Applied Sciences and Technology
ISSN (Print)2191-530X
ISSN (Electronic)2191-5318

ASJC Scopus subject areas

  • Biotechnology
  • General Chemical Engineering
  • General Mathematics
  • General Materials Science
  • Energy Engineering and Power Technology
  • General Engineering


Dive into the research topics of 'Interactive Theorem Proving'. Together they form a unique fingerprint.

Cite this