Formal Analysis of Future Energy Systems Using Interactive Theorem Proving

2022 ◽  
Author(s):  
Asad Ahmed ◽  
Osman Hasan ◽  
Falah Awwad ◽  
Nabil Bastaki
Keyword(s):  
Theorem Proving ◽  
Formal Analysis ◽  
Energy Systems ◽  
Interactive Theorem Proving

scholarly journals Preface

2011 ◽  
Vol 21 (4) ◽  
pp. 671-677 ◽  
Author(s):  
GÉRARD HUET
Keyword(s):  
Mathematical Logic ◽  
Computer Science ◽  
20Th Century ◽  
Theorem Proving ◽  
Propositional Calculus ◽  
Interactive Theorem Proving ◽  
Predicate Calculus ◽  
Special Issue ◽  
Mathematical Structures ◽  
Infinite Domains

This special issue of Mathematical Structures in Computer Science is devoted to the theme of ‘Interactive theorem proving and the formalisation of mathematics’.The formalisation of mathematics started at the turn of the 20th century when mathematical logic emerged from the work of Frege and his contemporaries with the invention of the formal notation for mathematical statements called predicate calculus. This notation allowed the formulation of abstract general statements over possibly infinite domains in a uniform way, and thus went well beyond propositional calculus, which goes back to Aristotle and only allowed tautologies over unquantified statements.

scholarly journals Practal — Practical Logic: A Bicycle for Your Mathematical Mind

2021 ◽  
Author(s):  
Steven Obua
Keyword(s):  
Theorem Proving ◽  
Interactive Theorem Proving ◽  
Mathematical Mind ◽  
Practical Logic

This is a first sketch of the design of Practal, an interactive theorem proving system for practical logic.

Applications of Formalized Information Theory

2015 ◽  
pp. 159-178
Keyword(s):  
Information Theory ◽  
Data Compression ◽  
Theorem Proving ◽  
Formal Analysis ◽  
Theoretic Analysis ◽  
Information Theoretic ◽  
Wide Range ◽  
Comprehensive Framework

In previous chapters, the authors provided a comprehensive framework that can be used in the formal probabilistic and information-theoretic analysis of a wide range of systems and protocols. In this chapter, they illustrate the usefulness of conducting this analysis using theorem proving by tackling a number of applications including a data compression application, the formal analysis of an anonymity-based MIX channel, and the properties of the onetime pad encryption system.

Sign in / Sign up

Export Citation Format

Share Document