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

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

1 2 3 ... 24 25 26 next

  1. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  2. 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)
  3. Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (2020)
  4. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  5. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  6. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  7. Elderhalli, Yassmeen; Hasan, Osman; Tahar, Sofiène: A framework for formal dynamic dependability analysis using HOL theorem proving (2020)
  8. Gauthier, Thibault: Tree neural networks in HOL4 (2020)
  9. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  10. Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
  11. Kovács, Laura; Lachnitt, Hanna; Szeider, Stefan: Formalizing graph trail properties in Isabelle/HOL (2020)
  12. Nagashima, Yutaka: Simple dataset for proof method recommendation in Isabelle/HOL (2020)
  13. Rashid, Adnan; Hasan, Osman: Formal verification of robotic cell injection systems up to 4-DOF using \textsfHOLLight (2020)
  14. Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
  15. Sheng, Feng; Zhu, Huibiao; He, Jifeng; Yang, Zongyuan; Bowen, Jonathan P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP (2020)
  16. Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
  17. Syeda, Hira Taqdees; Klein, Gerwin: Formal reasoning under cached address translation (2020)
  18. Tian, Chun; Sangiorgi, Davide: Unique solutions of contractions, CCS, and their HOL formalisation (2020)
  19. Bishop, Steve; Fairbairn, Matthew; Mehnert, Hannes; Norrish, Michael; Ridge, Tom; Sewell, Peter; Smith, Michael; Wansbrough, Keith: Engineering with logic. Rigorous test-oracle specification and validation for TCP/IP and the sockets API (2019)
  20. Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René: Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL (2019)

1 2 3 ... 24 25 26 next