
ACL2s
 Referenced in 11 articles
[sw07734]
 latest inception of the BoyerMoore theorem prover, the 2005 recipient of the ACM software...

Kit
 Referenced in 7 articles
[sw22321]
 mechanically checked with the BoyerMoore theorem prover...

PREVAIL
 Referenced in 7 articles
[sw02114]
 form acceptable by the BoyerMoore theorem prover. For well identified classes of circuits...

Imandra
 Referenced in 1 article
[sw37911]
 describe Imandra, a modern computational logic theorem prover designed to bridge the gap between decision ... semiautomatic inductive provers of the BoyerMoore family like ACL2, and interactive proof assistants...

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

OMRS
 Referenced in 39 articles
[sw03359]
 Communication protocols for mathematical services based on KQML...

Haskell
 Referenced in 851 articles
[sw03521]
 Haskell is a standardized, generalpurpose purely functional...

HOL
 Referenced in 508 articles
[sw05492]
 Higher Order Logic (HOL) is a programming environment...

OCaml
 Referenced in 271 articles
[sw06363]
 OCaml is the most popular variant of the...

Nuprl
 Referenced in 389 articles
[sw06751]
 The Nuprl system is a framework for reasoning...

LISP
 Referenced in 126 articles
[sw07201]
 Lisp (historically, LISP) is a family of computer...

NQTHM
 Referenced in 149 articles
[sw07543]
 A computational logic handbook. This book is a...

LCF
 Referenced in 157 articles
[sw08360]
 Edinburgh LCF. A mechanized logic of computation. From...

UNITY
 Referenced in 184 articles
[sw13461]
 Simulation model development and analysis in UNITY. We...

CLAM
 Referenced in 39 articles
[sw19619]
 CLAM Proof Planner. OYSTER is an interactive proof...

Oyster
 Referenced in 32 articles
[sw19629]
 Theorem proving and program synthesis with Oyster. Martin...

Piton
 Referenced in 11 articles
[sw28721]
 Piton: A verified assembly level language. Mountaineers use...