• HOL Light

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

  • Referenced in 15 articles [sw18516]
  • agent-based deduction system for classical higher-order logic is developed. Leo-III combines ... native support for reasoning in expressive non-classical logics...
  • AUTO2

  • Referenced in 6 articles [sw17595]
  • theorem prover for classical higher-order logic named auto2. The prover is designed to make...
  • GoedelGod

  • Referenced in 7 articles [sw32223]
  • modeled as a fragment of classical higher-order logic (HOL); thus, the formalization is essentially...
  • embed_modal

  • Referenced in 3 articles [sw28304]
  • higher-order modal logic into classical higher-order logic. The procedure was implemented...
  • FMLtoHOL

  • Referenced in 3 articles [sw21539]
  • modeled as natural fragments of classical higher-order logic (HOL). The FMLtoHOL tool exploits this...
  • RALL

  • Referenced in 9 articles [sw08505]
  • language of heterogeneous relation algebra including higher-order operators and domain constructions, and checks ... relation-algebraic and predicate-logical formulas, relying on the classical universal-algebraic concepts of atom...
  • Hintikka's world

  • Referenced in 2 articles [sw31988]
  • shows intelligent artificial agents reasoning about higher-order knowledge (a knows that b knows that ... clicking on them. It contains many classical AI examples. It is a tribute to Jaakko ... tool can be used for: learning modal logic, model checking and satisfiability problem; learning models...
  • Paraconsistency

  • Referenced in 1 article [sw28572]
  • Classical Logics 2005). We limit ourselves to the propositional fragment of the higher-order logic...
  • ANSYS

  • Referenced in 677 articles [sw00044]
  • ANSYS offers a comprehensive software suite that spans...
  • ACL2

  • Referenced in 281 articles [sw00060]
  • ACL2 is both a programming language in which...
  • Coq

  • Referenced in 1845 articles [sw00161]
  • Coq is a formal proof management system. It...
  • Dafny

  • Referenced in 70 articles [sw00183]
  • Dafny is an imperative object-based language with...
  • GAP

  • Referenced in 3026 articles [sw00320]
  • GAP is a system for computational discrete algebra...
  • Isabelle

  • Referenced in 667 articles [sw00454]
  • Isabelle is a generic proof assistant. It allows...
  • LEO-II

  • Referenced in 51 articles [sw00512]
  • LEO-II is a standalone, resolution-based higher...
  • Maple

  • Referenced in 5253 articles [sw00545]
  • The result of over 30 years of cutting...
  • Mathematica

  • Referenced in 6166 articles [sw00554]
  • Almost any workflow involves computing results, and that...
  • Matlab

  • Referenced in 12821 articles [sw00558]
  • MATLAB® is a high-level language and interactive...
  • Nitpick

  • Referenced in 61 articles [sw00622]
  • Nitpick is a counterexample generator for Isabelle/HOL that...