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/)
Keywords for this software
References in zbMATH (referenced in 508 articles , 1 standard article )
Showing results 1 to 20 of 508.
Sorted by year (- Abrahamsson, Oskar: A verified proof checker for higher-order logic (2020)
- 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)
- Ahmad, Waqar; Hasan, Osman; Tahar, Sofiène: Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation (2020)
- Barbosa, Haniel; Blanchette, Jasmin Christian; Fleury, Mathias; Fontaine, Pascal: Scalable fine-grained proofs for formula processing (2020)
- Basin, David A.; Lochbihler, Andreas; Sefidgar, S. Reza: CryptHOL: game-based proofs in higher-order logic (2020)
- Benzmüller, Christoph; Scott, Dana S.: Automating free logic in HOL, with an experimental application in category theory (2020)
- Elderhalli, Yassmeen; Hasan, Osman; Tahar, Sofiène: A framework for formal dynamic dependability analysis using HOL theorem proving (2020)
- Gauthier, Thibault: Tree neural networks in HOL4 (2020)
- Gheri, Lorenzo; Popescu, Andrei: A formalized general theory of syntax with bindings: extended version (2020)
- Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
- Kovács, Laura; Lachnitt, Hanna; Szeider, Stefan: Formalizing graph trail properties in Isabelle/HOL (2020)
- Nagashima, Yutaka: Simple dataset for proof method recommendation in Isabelle/HOL (2020)
- Rashid, Adnan; Hasan, Osman: Formal verification of robotic cell injection systems up to 4-DOF using \textsfHOLLight (2020)
- Schlichtkrull, Anders; Blanchette, Jasmin; Traytel, Dmitriy; Waldmann, Uwe: Formalizing Bachmair and Ganzinger’s ordered resolution prover (2020)
- 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)
- Shi, Zhiping; Guan, Yong; Li, Ximeng: Formalization of complex analysis and matrix theory (2020)
- Syeda, Hira Taqdees; Klein, Gerwin: Formal reasoning under cached address translation (2020)
- Tian, Chun; Sangiorgi, Davide: Unique solutions of contractions, CCS, and their HOL formalisation (2020)
- 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)
- Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René: Verifying an incremental theory solver for linear arithmetic in Isabelle/HOL (2019)