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

HOL Light
 Referenced in 272 articles
[sw06580]
 interactive proof assistant for classical higherorder logic, intended as a clean and simplified version...

ETPS
 Referenced in 149 articles
[sw06302]
 automated theoremprover for firstorder logic and type theory. The latter ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higherorder logic. It has a formula editor which...

CASL
 Referenced in 159 articles
[sw02235]
 various sublanguages. It has extensions to higherorder, statebased, concurrent, and other languages...

LCF
 Referenced in 151 articles
[sw08360]
 proof assistant for higher order logic originally developed for reasoning about hardware.2 The multifaceted...

Sledgehammer
 Referenced in 104 articles
[sw07047]
 tool that harnesses external firstorder automatic theorem provers (ATPs) to discharge interactive proof obligations ... Satallax, the two most prominent higherorder ATPs, improving its performance on higherorder problems...

PROST
 Referenced in 140 articles
[sw12822]
 NavierStokes solver, and a higher order interface advection scheme. The curvature to the interface...

LISP
 Referenced in 122 articles
[sw07201]
 automatic storage management, dynamic typing, conditionals, higherorder functions, recursion, and the selfhosting compiler...

LEGO
 Referenced in 105 articles
[sw09685]
 that of informal mathematics. The higherorder power of its underlying type theories...

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

TPS
 Referenced in 68 articles
[sw00973]
 automated theoremprover for firstorder logic and type theory. The latter ... prove theorems of first and higherorder logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higherorder logic. It has a formula editor which...

GHC
 Referenced in 87 articles
[sw06691]
 Glasgow Haskell Compiler inliner. Higherorder languages such as Haskell encourage the programmer to build...

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

Pict
 Referenced in 70 articles
[sw08929]
 data structures, protocols for returning results, higherorder programming, selective communication, and concurrent objects...

LEOII
 Referenced in 42 articles
[sw00512]
 standalone, resolutionbased higherorder theorem prover designed for fruitful cooperation with specialist provers ... natural fragments of higherorder logic. At present LEOII can cooperate with TPTP compliant ... firstorder automated theorem provers such as E, SPASS, Gandalf and Vampire. World Champion ... division (automation of higherorder logic) at CASCJ5. At CASC...

Coq/SSReflect
 Referenced in 60 articles
[sw09360]
 Colour Theorem and which leverages the higherorder nature of Coq’s underlying logic...

Satallax
 Referenced in 39 articles
[sw06849]
 automated theorem prover for higherorder logic. The particular form of higherorder logic supported...

ProofPower
 Referenced in 51 articles
[sw06339]
 tool based on an implementation of Higher Order Logic (HOL), following the LCF paradigm...

Nitpick
 Referenced in 48 articles
[sw00622]
 builds on Kodkod, a SATbased firstorder relational model finder. Nitpick supports unbounded quantification ... counterexamples than other model finders for higherorder logic, without restrictions on the form...

Ynot
 Referenced in 34 articles
[sw12334]
 supports writing, reasoning about, and extracting higherorder, dependentlytyped programs with sideeffects ... abstraction mechanisms of Coq to build higherlevel reasoning mechanisms which in turn ... finite maps, including support for a higherorder (effectful) iterator. The implementations range from simple...