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 588 articles , 1 standard article )

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

1 2 3 ... 28 29 30 next

  1. Abbasi, Rosa; Schiffl, Jonas; Darulova, Eva; Ulbrich, Mattias; Ahrendt, Wolfgang: Deductive verification of floating-point Java programs in KeY (2021)
  2. Abdelghany, Mohamed; Tahar, Sofiène: Formalization of RBD-based cause consequence analysis in HOL (2021)
  3. Bentkamp, Alexander; Blanchette, Jasmin; Tourret, Sophie; Vukmirović, Petar; Waldmann, Uwe: Superposition with lambdas (2021)
  4. Chan, Hing Lun; Norrish, Michael: Mechanisation of the AKS algorithm (2021)
  5. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  6. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  7. From, Asta Halkjær; Eschen, Agnes Moesgård; Villadsen, Jørgen: Formalizing axiomatic systems for propositional logic in Isabelle/HOL (2021)
  8. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  9. 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)
  10. Haslbeck, Maximilian P. L.; Lammich, Peter: For a few dollars more. Verified fine-grained algorithm analysis down to LLVM (2021)
  11. Holub, Štěpán; Starosta, Štěpán: Binary intersection formalized (2021)
  12. Maletzky, Alexander: A generic and executable formalization of signature-based Gröbner basis algorithms (2021)
  13. Steen, Alexander; Benzmüller, Christoph: Extensional higher-order paramodulation in Leo-III (2021)
  14. Streit, David: Experiments in causality and STIT (2021)
  15. Sutcliffe, Geoff: The 10th IJCAR automated theorem proving system competition -- CASC-J10 (2021)
  16. Tan, Yong Kiam; Heule, Marijn J. H.; Myreen, Magnus O.: \textttcake_lpr: verified propagation redundancy checking in CakeML (2021)
  17. Xu, Runqing; Li, Liming; Zhan, Bohua: Verified interactive computation of definite integrals (2021)
  18. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  19. 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)
  20. Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (2020)

1 2 3 ... 28 29 30 next