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

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

1 2 3 ... 13 14 15 next

  1. Arthan, Rob: On definitions of constants and types in HOL (2016)
  2. Bengtson, Jesper; Parrow, Joachim; Weber, Tjark: Psi-calculi in Isabelle (2016)
  3. Blanchette, Jasmin Christian; Böhme, Sascha; Fleury, Mathias; Smolka, Steffen Juilf; Steckermeier, Albert: Semi-intelligible Isar proofs from machine-generated proofs (2016)
  4. Kumar, Ramana; Arthan, Rob; Myreen, Magnus O.; Owens, Scott: Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation (2016)
  5. Qasim, Muhammad; Hasan, Osman; Elleuch, Maissa; Tahar, Sofiène: Formalization of normal random variables in HOL (2016)
  6. Rabe, Florian: The future of logic: foundation-independence (2016)
  7. Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)
  8. Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)
  9. Benzmüller, Christoph; Sultana, Nik; Paulson, Lawrence C.; Theiß, Frank: The higher-order prover Leo-II (2015)
  10. Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
  11. Elleuch, Maissa; Hasan, Osman; Tahar, Sofiène; Abid, Mohamed: Formal probabilistic analysis of detection properties in wireless sensor networks (2015)
  12. Fox, Anthony: Improved tool support for machine-code decompilation in HOL4 (2015)
  13. Kaliszyk, Cezary; Urban, Josef: HOL(y)Hammer: online ATP service for HOL Light (2015)
  14. Noschinski, Lars: A graph library for Isabelle (2015)
  15. Pąk, Karol: Improving legibility of formal proofs based on the close reference principle is NP-hard (2015)
  16. Abbasi, Naeem; Hasan, Osman; Tahar, Sofiène: An approach for lifetime reliability analysis using theorem proving (2014)
  17. Ahmed, Waqar; Hasan, Osman; Tahar, Sofiene; Hamdi, Mohammad Salah: Towards the formal reliability analysis of oil and gas pipelines (2014)
  18. Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
  19. Aravantinos, Vincent; Tahar, Sofiène: Implicational rewriting tactics in HOL (2014)
  20. Banach, Richard; Zhu, Huibiao; Su, Wen; Huang, Runlei: Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application (2014)

1 2 3 ... 13 14 15 next