TY - CHAP
T1 - Interactive Theorem Proving
AU - Ahmed, Asad
AU - Hasan, Osman
AU - Awwad, Falah
AU - Bastaki, Nabil
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85113471086&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85113471086&partnerID=8YFLogxK
U2 - 10.1007/978-3-030-78409-6_2
DO - 10.1007/978-3-030-78409-6_2
M3 - Chapter
AN - SCOPUS:85113471086
T3 - SpringerBriefs in Applied Sciences and Technology
SP - 23
EP - 29
BT - SpringerBriefs in Applied Sciences and Technology
PB - Springer Science and Business Media Deutschland GmbH
ER -