HOL

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

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

1 2 3 ... 25 26 27 next

  1. Färber, Michael; Kaliszyk, Cezary; Urban, Josef: Machine learning guidance for connection tableaux (2021)
  2. Fervari, Raul; Trucco, Francisco; Ziliani, Beta: Verification of dynamic bisimulation theorems in Coq (2021)
  3. Gauthier, Thibault; Kaliszyk, Cezary; Urban, Josef; Kumar, Ramana; Norrish, Michael: TacticToe: learning to prove with tactics (2021)
  4. 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)
  5. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  6. 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)
  7. Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (2020)
  8. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  9. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  10. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  11. Berghammer, Rudolf; Furusawa, Hitoshi; Guttmann, Walter; Höfner, Peter: Relational characterisations of paths (2020)
  12. Elderhalli, Yassmeen; Hasan, Osman; Tahar, Sofiène: A framework for formal dynamic dependability analysis using HOL theorem proving (2020)
  13. Gauthier, Thibault: Tree neural networks in HOL4 (2020)
  14. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  15. Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
  16. Kovács, Laura; Lachnitt, Hanna; Szeider, Stefan: Formalizing graph trail properties in Isabelle/HOL (2020)
  17. Nagashima, Yutaka: Simple dataset for proof method recommendation in Isabelle/HOL (2020)
  18. Rashid, Adnan; Hasan, Osman: Formal verification of robotic cell injection systems up to 4-DOF using \textsfHOLLight (2020)
  19. Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
  20. 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)

1 2 3 ... 25 26 27 next