• ETPS

  • Referenced in 127 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...
  • HOL Light

  • Referenced in 138 articles [sw06580]
  • interactive proof assistant for classical higher-order logic, intended as a clean and simplified version...
  • TPS

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

  • Referenced in 35 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...
  • LEO-II

  • Referenced in 29 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...
  • Lambda-Clam

  • Referenced in 19 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...
  • Satallax

  • Referenced in 17 articles [sw06849]
  • automated theorem prover for higher-order logic. The particular form of higher-order logic supported...
  • HOL-OCL

  • Referenced in 20 articles [sw05734]
  • Object Constraint Language (OCL) in higher-order logic, we explore several key issues...
  • CCSL

  • Referenced in 19 articles [sw03357]
  • CCSL compiler translates CCSL specifications into higher-order logic either...
  • Nitpick

  • Referenced in 18 articles [sw00622]
  • counterexamples than other model finders for higher-order logic, without restrictions on the form...
  • HasCasl

  • Referenced in 11 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...
  • Ciao

  • Referenced in 27 articles [sw12088]
  • purpose programming language which supports logic, constraint, functional, higher-order, and object-oriented programming styles...
  • Coq/SSReflect

  • Referenced in 43 articles [sw09360]
  • which leverages the higher-order nature of Coq’s underlying logic to provide effective automation...
  • Athena

  • Referenced in 8 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...
  • THF0

  • Referenced in 8 articles [sw03310]
  • higher-order logic. Maintaining a consistent style between the first-order and higher-order languages...
  • CFML

  • Referenced in 7 articles [sw13287]
  • pure Caml program, this tool generates a logical formula that implies any valid post-condition ... that they are expressible in standard higher-order logic, allowing to exploit them in practice...
  • Predator

  • Referenced in 9 articles [sw07396]
  • inspired by works on separation logic with higher-order list predicates, but they...
  • Hiord

  • Referenced in 3 articles [sw07313]
  • Hiord: A type-free higher-order logic programming language with predicate abstraction A new formalism ... called Hiord, for defining type-free higher-order logic programming languages with predicate abstraction...
  • OMEGA

  • Referenced in 4 articles [sw19623]
  • Ωmega: A theorem prover for higher-order logic based on proof planning...
  • 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 higher-order logic and supply explicit machine-checkable proof...