Higher Order Logic (HOL) is a programming environment in which theorems can be proved and proof tools implemented. Built-in decision procedures and theorem provers can automatically establish many simple theorems. An Oracle mechanism gives access to external programs such as SAT and BDD engines. HOL 4 is particularly suitable as a platform for implementing combinations of deduction, execution, and property checking. (Source: http://freecode.com/)

References in zbMATH (referenced in 556 articles , 1 standard article )

Showing results 1 to 20 of 556.
Sorted by year (citations)

1 2 3 ... 26 27 28 next

  1. Chan, Hing Lun; Norrish, Michael: Mechanisation of the AKS algorithm (2021)
  2. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  3. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  4. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  5. Guan, Yong; Zhang, Jingzhi; Wang, Guohui; Li, Ximeng; Shi, Zhiping; Li, Yongdong: Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (2021)
  6. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  7. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  8. Abrahamsson, Oskar; Ho, Son; Kanabar, Hrutvik; Kumar, Ramana; Myreen, Magnus O.; Norrish, Michael; Tan, Yong Kiam: Proof-producing synthesis of CakeML from monadic HOL functions (2020)
  9. Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (2020)
  10. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  11. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  12. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  13. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  14. Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias: Verified analysis of random binary tree structures (2020)
  15. Echenim, Mnacho; Guiol, Hervé; Peltier, Nicolas: Formalizing the Cox-Ross-Rubinstein pricing of European derivatives in Isabelle/HOL (2020)
  16. Elderhalli, Yassmeen; Hasan, Osman; Tahar, Sofiène: A framework for formal dynamic dependability analysis using HOL theorem proving (2020)
  17. Gauthier, Thibault: Tree neural networks in HOL4 (2020)
  18. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  19. Joosten, Sebastiaan J. C.; Thiemann, René; Yamada, Akihisa: A verified implementation of algebraic numbers in Isabelle/HOL (2020)
  20. Kaufmann, Matt; Moore, J Strother: Limited second-order functionality in a first-order setting (2020)

1 2 3 ... 26 27 28 next