
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 higherorder logic, intended as a clean and simplified version...

ETPS
 Referenced in 145 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 147 articles
[sw08360]
 proof assistant for higher order logic originally developed for reasoning about hardware.2 The multifaceted...

Sledgehammer
 Referenced in 101 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 135 articles
[sw12822]
 NavierStokes 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, higherorder functions, recursion, and the selfhosting compiler...

LEGO
 Referenced in 104 articles
[sw09685]
 that of informal mathematics. The higherorder 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 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 86 articles
[sw06691]
 Glasgow Haskell Compiler inliner. Higherorder languages such as Haskell encourage the programmer to build...

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

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

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 56 articles
[sw09360]
 Colour Theorem and which leverages the higherorder nature of Coq’s underlying logic...

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

Ciao
 Referenced in 46 articles
[sw12088]
 language which supports logic, constraint, functional, higherorder, and objectoriented programming styles. Its main...

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

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