-
HOL Light
- Referenced in 293 articles
[sw06580]
- interactive proof assistant for classical higher-order logic, intended as a clean and simplified version...
-
ETPS
- Referenced in 156 articles
[sw06302]
- automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...
-
TPS
- Referenced in 71 articles
[sw00973]
- automated theorem-prover for first-order logic and type theory. The latter ... prove theorems of first- and higher-order logic interactively, automatically, or in a mixture ... proofs, and solving unification problems in higher-order logic. It has a formula editor which...
-
Satallax
- Referenced in 50 articles
[sw06849]
- automated theorem prover for higher-order logic. The particular form of higher-order logic supported...
-
LEO-II
- Referenced in 51 articles
[sw00512]
- specialist provers for natural fragments of higher-order logic. At present LEO-II can cooperate ... division (automation of higher-order logic) at CASC-J5. At CASC...
-
HiLog
- Referenced in 47 articles
[sw01580]
- HiLog: A foundation for higher-order logic programming. We describe a novel logic, called HiLog ... than does traditional predicate logic. HiLog has a higher-order syntax and allows arbitrary terms ... discussed, including DCG grammars, higher-order and modular logic programming, and deductive databases...
-
Nitpick
- Referenced in 61 articles
[sw00622]
- counterexamples than other model finders for higher-order logic, without restrictions on the form...
-
Lambda-Clam
- Referenced in 24 articles
[sw19614]
- domains: System description: Proof planning in higher-order logic with λClam. This system description outlines ... λClam system for proof planning in higher-order logic. The usefulness and feasibility of applying...
-
OMEGA
- Referenced in 32 articles
[sw19623]
- Ωmega: A theorem prover for higher-order logic based on proof planning...
-
Transfer
- Referenced in 26 articles
[sw21009]
- ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library...
-
Lifting
- Referenced in 26 articles
[sw21010]
- ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library...
-
CCSL
- Referenced in 25 articles
[sw03357]
- CCSL compiler translates CCSL specifications into higher-order logic either...
-
Ciao
- Referenced in 47 articles
[sw12088]
- purpose programming language which supports logic, constraint, functional, higher-order, and object-oriented programming styles...
-
HasCasl
- Referenced in 17 articles
[sw00399]
- expressive standard language for higher-order logic. Distinctive features of HasCasl include partial higher-order ... functions, higher-order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HasCasl provides ... effects, including a monad-based generic Hoare logic...
-
HOL-OCL
- Referenced in 21 articles
[sw05734]
- Object Constraint Language (OCL) in higher-order logic, we explore several key issues...
-
Coq/SSReflect
- Referenced in 66 articles
[sw09360]
- which leverages the higher-order nature of Coq’s underlying logic to provide effective automation...
-
THF0
- Referenced in 14 articles
[sw03310]
- higher-order logic. Maintaining a consistent style between the first-order and higher-order languages...
-
Leo-III
- Referenced in 14 articles
[sw18516]
- agent-based deduction system for classical higher-order logic is developed. Leo-III combines...
-
Athena
- Referenced in 10 articles
[sw09967]
- programming language, Athena is a higher-order functional language in the tradition of Scheme ... many-sorted first-order logic. Many-sorted first-order logic is a very expressive language ... Manzano in her ”Extensions of first-order logic”) have argued that it can be viewed ... framework for all other logics, including higher-order logic. It retains the tractability of first...
-
Predator
- Referenced in 17 articles
[sw07396]
- inspired by works on separation logic with higher-order list predicates, but they...