• 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 first-order 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 SAT-solver. MiniSat is a minimalistic...
  • SETHEO

  • Referenced in 119 articles [sw00707]
  • SETHEO: A high-performance theorem prover. The paper...
  • PLUMP

  • Referenced in 14 articles [sw00718]
  • The joint CSCS-ETH/NEC collaboration in parallel...
  • SageMath

  • Referenced in 1675 articles [sw00825]
  • Sage (SageMath) is free, open-source 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, general-purpose purely functional...
  • Eiffel

  • Referenced in 290 articles [sw03522]
  • Eiffel is an ISO-standardized, object-oriented programming...
  • SPASS

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