
ModGen
 Referenced in 6 articles
[sw21347]
 complete theorem prover for first order logic with finite Herbrand domains. ModGen takes first order ... problems which are hard for general resolution theorem provers are found easy for ModGen...

Slakje
 Referenced in 1 article
[sw33644]
 Herbrand constructivization for automated intuitionistic theorem proving. We describe a new method to constructivize proofs ... based on Herbrand disjunctions by giving a practically effective algorithm that converts (some) classical first ... Together with an automated classical firstorder theorem prover such a method yields an (incomplete...

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

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

Magma
 Referenced in 2917 articles
[sw00540]
 Computer algebra system (CAS). Magma is a large...

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

Maxima
 Referenced in 154 articles
[sw00560]
 Maxima is a system for the manipulation of...

MiniSat
 Referenced in 536 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

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

PLUMP
 Referenced in 14 articles
[sw00718]
 The joint CSCSETH/NEC collaboration in parallel...

SageMath
 Referenced in 1675 articles
[sw00825]
 Sage (SageMath) is free, opensource math software...

TPS
 Referenced in 71 articles
[sw00973]
 TPS and ETPS are, respectively, the Theorem Proving...

PERL
 Referenced in 265 articles
[sw01225]
 Programming Perl. Perl is a language for easily...

TGTP
 Referenced in 5 articles
[sw01826]
 TGTP: The Great Theorem Prover. ...

CASL
 Referenced in 172 articles
[sw02235]
 The specification language developed by CoFI is called...

OTTER
 Referenced in 314 articles
[sw02904]
 Our current automated deduction system Otter is designed...

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

Eiffel
 Referenced in 290 articles
[sw03522]
 Eiffel is an ISOstandardized, objectoriented programming...

SPASS
 Referenced in 178 articles
[sw04108]
 SPASS is an automated theorem prover for first...