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

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

1 2 3 ... 20 21 22 next

  1. Gauthier, Thibault; Kaliszyk, Cezary: Aligning concepts across proof assistant libraries (2019)
  2. Kunčar, Ondřej; Popescu, Andrei: From types to sets by local type definition in higher-order logic (2019)
  3. Abdulaziz, Mohammad; Norrish, Michael; Gretton, Charles: Formally verified algorithms for upper-bounding state space diameters (2018)
  4. Bannister, Callum; Höfner, Peter; Klein, Gerwin: Backwards and forwards with separation logic (2018)
  5. Bottesch, Ralph; Haslbeck, Max W.; Thiemann, René: A verified efficient implementation of the LLL basis reduction algorithm (2018)
  6. Carette, Jacques; Farmer, William M.; Laskowski, Patrick: HOL Light QE (2018)
  7. Cauderlier, Raphaël: Tactics and certificates in Meta Dedukti (2018)
  8. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  9. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  10. Goertzel, Zarathustra; Jakubův, Jan; Schulz, Stephan; Urban, Josef: Proofwatch: watchlist guidance for large theories in E (2018)
  11. Guttmann, Walter: Verifying minimum spanning tree algorithms with Stone relation algebras (2018)
  12. Guttmann, Walter: An algebraic framework for minimum spanning tree problems (2018)
  13. Hupel, Lars; Nipkow, Tobias: A verified compiler from Isabelle/HOL to CakeML (2018)
  14. Maletzky, Alexander; Immler, Fabian: Gröbner bases of modules and Faugère’s (F_4) algorithm in Isabelle/HOL (2018)
  15. Melham, Tom: Symbolic trajectory evaluation (2018)
  16. Nagashima, Yutaka; Parsert, Julian: Goal-oriented conjecturing for Isabelle/HOL (2018)
  17. Paulson, Lawrence C.: Computational logic: its origins and applications (2018)
  18. Piotrowski, Bartosz; Urban, Josef: ATPboost: learning premise selection in binary setting with ATP feedback (2018)
  19. Shankar, Natarajan: Combining model checking and deduction (2018)
  20. Shi, Ling; Zhao, Yongxin; Liu, Yang; Sun, Jun; Dong, Jin Song; Qin, Shengchao: A UTP semantics for communicating processes with shared variables and its formal encoding in PVS (2018)

1 2 3 ... 20 21 22 next