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

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

ETPS
 Referenced in 158 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...

Sledgehammer
 Referenced in 128 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...

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

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

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

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

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

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

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

TPS
 Referenced in 71 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...

LEOII
 Referenced in 51 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...

HiLog
 Referenced in 49 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...

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

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

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

DiffSharp
 Referenced in 45 articles
[sw16033]
 Jacobianvector products) is applied using higherorder functions, that is, functions which take other ... meaning that you can compute exact higherorder derivatives or differentiate functions that are internally...

Nitpick
 Referenced in 61 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...

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