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

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

1 2 3 ... 23 24 25 next

  1. Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
  2. Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of ethernet based communication networks in a smart grid substation (2020)
  3. Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
  4. Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
  5. Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
  6. Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
  7. Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
  8. Rashid, Adnan; Hasan, Osman: Formal verification of robotic cell injection systems up to 4-DOF using \textsfHOLLight (2020)
  9. 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)
  10. Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
  11. Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René: Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL (2019)
  12. Brown, Chad E.; Gauthier, Thibault; Kaliszyk, Cezary; Sutcliffe, Geoff; Urban, Josef: GRUNGE: a grand unified ATP challenge (2019)
  13. Chvalovský, Karel; Jakubův, Jan; Suda, Martin; Urban, Josef: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for (\mathrmE) (2019)
  14. Eberl, Manuel: Verifying randomised social choice (2019)
  15. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  16. Hupel, Lars: Certifying dictionary construction in Isabelle/HOL (2019)
  17. Kiam Tan, Yong; Myreen, Magnus O.; Kumar, Ramana; Fox, Anthony; Owens, Scott; Norrish, Michael: The verified CakeML compiler backend (2019)
  18. Kunčar, Ondřej; Popescu, Andrei: A consistent foundation for Isabelle/HOL (2019)
  19. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  20. Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong: Formalization of geometric algebra in HOL Light (2019)

1 2 3 ... 23 24 25 next