• HOL

  • Referenced in 416 articles [sw05492]
  • Higher Order Logic (HOL) is a programming environment in which theorems can be proved...
  • HOL Light

  • Referenced in 253 articles [sw06580]
  • interactive proof assistant for classical higher-order logic, intended as a clean and simplified version...
  • ETPS

  • Referenced in 145 articles [sw06302]
  • automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...
  • CASL

  • Referenced in 159 articles [sw02235]
  • various sublanguages. It has extensions to higher-order, state-based, concurrent, and other languages...
  • LCF

  • Referenced in 147 articles [sw08360]
  • proof assistant for higher order logic originally developed for reasoning about hardware.2 The multi-faceted...
  • Sledgehammer

  • Referenced in 101 articles [sw07047]
  • tool that harnesses external first-order automatic theorem provers (ATPs) to discharge interactive proof obligations ... Satallax, the two most prominent higher-order ATPs, improving its performance on higher-order problems...
  • PROST

  • Referenced in 135 articles [sw12822]
  • Navier-Stokes solver, and a higher order interface advection scheme. The curvature to the interface...
  • LISP

  • Referenced in 120 articles [sw07201]
  • automatic storage management, dynamic typing, conditionals, higher-order functions, recursion, and the self-hosting compiler...
  • LEGO

  • Referenced in 104 articles [sw09685]
  • that of informal mathematics. The higher-order power of its underlying type theories...
  • ICALAB

  • Referenced in 95 articles [sw15047]
  • independent component analysis) employing HOS (higher order statistics), BSS (blind source separation) employing SOS (second...
  • TPS

  • Referenced in 67 articles [sw00973]
  • automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...
  • GHC

  • Referenced in 86 articles [sw06691]
  • Glasgow Haskell Compiler inliner. Higher-order languages such as Haskell encourage the programmer to build...
  • Pict

  • Referenced in 70 articles [sw08929]
  • data structures, protocols for returning results, higher-order programming, selective communication, and concurrent objects...
  • HiLog

  • Referenced in 43 articles [sw01580]
  • HiLog: A foundation for higher-order logic programming. We describe a novel logic, called HiLog ... traditional predicate logic. HiLog has a higher-order syntax and allows arbitrary terms to appear ... predicate calculus. But its semantics is first-order and admits a sound and complete proof ... HiLog are discussed, including DCG grammars, higher-order and modular logic programming, and deductive databases...
  • LEO-II

  • Referenced in 42 articles [sw00512]
  • standalone, resolution-based higher-order theorem prover designed for fruitful cooperation with specialist provers ... natural fragments of higher-order logic. At present LEO-II can cooperate with TPTP compliant ... first-order automated theorem provers such as E, SPASS, Gandalf and Vampire. World Champion ... division (automation of higher-order logic) at CASC-J5. At CASC...
  • Coq/SSReflect

  • Referenced in 56 articles [sw09360]
  • Colour Theorem and which leverages the higher-order nature of Coq’s underlying logic...
  • Satallax

  • Referenced in 37 articles [sw06849]
  • automated theorem prover for higher-order logic. The particular form of higher-order logic supported...
  • Ciao

  • Referenced in 46 articles [sw12088]
  • language which supports logic, constraint, functional, higher-order, and object-oriented programming styles. Its main...
  • Nitpick

  • Referenced in 46 articles [sw00622]
  • builds on Kodkod, a SAT-based first-order relational model finder. Nitpick supports unbounded quantification ... counterexamples than other model finders for higher-order logic, without restrictions on the form...
  • Lambda-Clam

  • Referenced in 24 articles [sw19614]
  • system that support proof planning over higher-order domains: System description: Proof planning in higher ... λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying ... higher-order proof planning to a number of types of problem is outlined, in particular ... hardware systems. The use of a higher-order metatheory overcomes problems encountered in Clam because...