HOL

HOL

HOL refers to a higher-order logic system that can be used as a verification framework for software and hardware, as well as a platform for formalizing pure mathematics. It is a meta-logic that models the semantics of other object-level logics and uses high-order logic theorem provers to reason in the context of these object-logics. The HOL system is also an interactive mechanized proof assistant.From: Handbook of RAMS in Railway Systems [2018], Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts [2020], Embedded Systems Handbook [2019]

Formal Reliability Analysis of Railway Systems Using Theorem Proving Technique

View Chapter

Purchase Book

Published in Qamar Mahboob, Enrico Zio, Handbook of RAMS in Railway Systems, 2018

Waqar Ahmad, Osman Hasan, Sofiène Tahar

HOL [30] is an interactive theorem prover developed at the University of Cambridge, United Kingdom, for conducting proofs in HOL. It utilizes the simple type theory of Church [31] along with Hindley–Milner polymorphism [32] to implement HOL. HOL has been successfully used as a verification framework for both software and hardware as well as a platform for the formalization of pure mathematics.

Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts

View Article

Journal Information

Published in Journal of Applied Non-Classical Logics, 2020

Ariel Jonathan Roffé

Also note that the same kinds of automatic calculations presented in this article can probably be carried out using other available software packages, based on different approaches. For example, the shallow semantical embeddings (SSE) approach utilises higher-order classical logic as a meta-logic, in which other object-level logics’ semantics are modelled; high-order logic theorem provers are then used to reason in the context of these object-logics (see Benzmüller, 2019 for an overview and some examples; one available software package for using this approach is Isabelle/HOL, see Nipkow, Paulson, & Wenzel, 2002). This approach has been fruitfully used within philosophy for studies in computational metaphysics (see Kirchner, Benzmüller & Zalta, 2019a, 2019b; and references therein).

Explore chapters and articles related to this topic

Formal Reliability Analysis of Railway Systems Using Theorem Proving Technique

Reconstructor: a computer program that uses three-valued logics to represent lack of information in empirical scientific contexts