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

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

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

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

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

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

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

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

HasCasl
 Referenced in 13 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...

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

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

Athena
 Referenced in 9 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...

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

CFML
 Referenced in 7 articles
[sw13287]
 pure Caml program, this tool generates a logical formula that implies any valid postcondition ... that they are expressible in standard higherorder logic, allowing to exploit them in practice...

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

Hiord
 Referenced in 3 articles
[sw07313]
 Hiord: A typefree higherorder logic programming language with predicate abstraction A new formalism ... called Hiord, for defining typefree higherorder logic programming languages with predicate abstraction...

VeriML
 Referenced in 4 articles
[sw13522]
 VeriML: typed computation of logical terms inside a language with effects. Modern proof assistants such ... because they support formal reasoning in higherorder logic and supply explicit machinecheckable proof...

AUTO2
 Referenced in 2 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...

LeoPARD
 Referenced in 3 articles
[sw13554]
 knowledge representation and reasoning tools for higherorder logic(s). It combines a sophisticated data...