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

LeoIII
 Referenced in 16 articles
[sw18516]
 agentbased deduction system for classical higherorder logic is developed. LeoIII combines ... native support for reasoning in expressive nonclassical logics...

AUTO2
 Referenced in 6 articles
[sw17595]
 theorem prover for classical higherorder logic named auto2. The prover is designed to make...

GoedelGod
 Referenced in 7 articles
[sw32223]
 modeled as a fragment of classical higherorder logic (HOL); thus, the formalization is essentially...

embed_modal
 Referenced in 4 articles
[sw28304]
 higherorder modal logic into classical higherorder logic. The procedure was implemented...

FMLtoHOL
 Referenced in 4 articles
[sw21539]
 modeled as natural fragments of classical higherorder logic (HOL). The FMLtoHOL tool exploits this...

RALL
 Referenced in 9 articles
[sw08505]
 language of heterogeneous relation algebra including higherorder operators and domain constructions, and checks ... relationalgebraic and predicatelogical formulas, relying on the classical universalalgebraic concepts of atom...

Hintikka's world
 Referenced in 2 articles
[sw31988]
 shows intelligent artificial agents reasoning about higherorder 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 higherorder logic...

ACL2
 Referenced in 283 articles
[sw00060]
 ACL2 is both a programming language in which...

Coq
 Referenced in 1880 articles
[sw00161]
 Coq is a formal proof management system. It...

Dafny
 Referenced in 72 articles
[sw00183]
 Dafny is an imperative objectbased language with...

GAP
 Referenced in 3154 articles
[sw00320]
 GAP is a system for computational discrete algebra...

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

LEOII
 Referenced in 51 articles
[sw00512]
 LEOII is a standalone, resolutionbased higher...

Maple
 Referenced in 5363 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 6337 articles
[sw00554]
 Almost any workflow involves computing results, and that...

Matlab
 Referenced in 13460 articles
[sw00558]
 MATLAB® is a highlevel language and interactive...

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

SETHEO
 Referenced in 122 articles
[sw00707]
 SETHEO: A highperformance theorem prover. The paper...