
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...

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...

HiLog
 Referenced in 45 articles
[sw01580]
 HiLog: A foundation for higherorder logic programming. We describe a novel logic, called HiLog ... than does traditional predicate logic. HiLog has a higherorder syntax and allows arbitrary terms ... discussed, including DCG grammars, higherorder and modular logic programming, and deductive databases...

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

LEOII
 Referenced in 42 articles
[sw00512]
 specialist provers for natural fragments of higherorder logic. At present LEOII can cooperate ... division (automation of higherorder logic) at CASCJ5. At CASC...

Nitpick
 Referenced in 48 articles
[sw00622]
 counterexamples than other model finders for higherorder logic, without restrictions on the form...

LambdaClam
 Referenced in 24 articles
[sw19614]
 domains: System description: Proof planning in higherorder logic with λClam. This system description outlines ... λClam system for proof planning in higherorder logic. The usefulness and feasibility of applying...

OMEGA
 Referenced in 26 articles
[sw19623]
 Ωmega: A theorem prover for higherorder logic based on proof planning...

CCSL
 Referenced in 25 articles
[sw03357]
 CCSL compiler translates CCSL specifications into higherorder logic either...

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

Transfer
 Referenced in 22 articles
[sw21009]
 ubiquitous in formal reasoning with higherorder logic. Typically, users want to build a library...

Lifting
 Referenced in 22 articles
[sw21010]
 ubiquitous in formal reasoning with higherorder logic. Typically, users want to build a library...

HOLOCL
 Referenced in 21 articles
[sw05734]
 Object Constraint Language (OCL) in higherorder logic, we explore several key issues...

HasCasl
 Referenced in 16 articles
[sw00399]
 expressive standard language for higherorder logic. Distinctive features of HasCasl include partial higherorder ... functions, higherorder subtyping, shallow polymorphism, and an extensive typeclass mechanism. Moreover, HasCasl provides ... effects, including a monadbased generic Hoare logic...

Coq/SSReflect
 Referenced in 60 articles
[sw09360]
 which leverages the higherorder nature of Coq’s underlying logic to provide effective automation...

THF0
 Referenced in 12 articles
[sw03310]
 higherorder logic. Maintaining a consistent style between the ﬁrstorder and higherorder languages...

Athena
 Referenced in 10 articles
[sw09967]
 programming language, Athena is a higherorder functional language in the tradition of Scheme ... manysorted firstorder logic. Manysorted firstorder logic is a very expressive language ... Manzano in her ”Extensions of firstorder logic”) have argued that it can be viewed ... framework for all other logics, including higherorder logic. It retains the tractability of first...

Predator
 Referenced in 16 articles
[sw07396]
 inspired by works on separation logic with higherorder list predicates, but they...

AUTO2
 Referenced in 6 articles
[sw17595]
 saturationbased heuristic prover for higherorder logic. We introduce a new theorem prover ... classical higherorder logic named auto2. The prover is designed to make use of human...