• SETHEO

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

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

  • Referenced in 225 articles [sw02904]
  • Our current automated deduction system Otter is designed...
  • Prover9

  • Referenced in 106 articles [sw04969]
  • Prover9 and Mace4: Prover9 is an automated theorem...
  • MUSCADET

  • Referenced in 7 articles [sw06859]
  • MUSCADET: An automatic theorem proving system using knowledge...
  • Mace4

  • Referenced in 132 articles [sw06905]
  • finite model-finder Mace4. Mace4 is a program...
  • NQTHM

  • Referenced in 86 articles [sw07543]
  • A computational logic handbook This book is a...
  • LCF

  • Referenced in 107 articles [sw08360]
  • Edinburgh LCF. A mechanized logic of computation. From...
  • IMPS

  • Referenced in 30 articles [sw09143]
  • IMPS: An interactive mathematical proof system. IMPS is...
  • SAD

  • Referenced in 12 articles [sw09796]
  • System for automated deduction (SAD): A tool for...
  • MKRP

  • Referenced in 3 articles [sw19606]
  • The Markgraph Karl Refutation Procedure, a graph-based...
  • InKa

  • Referenced in 11 articles [sw19610]
  • InKa - an inductive theorem prover. InKa: INduktionsbeweiser KArlsruhe...
  • SNARK

  • Referenced in 3 articles [sw19611]
  • SNARK - SRI’s New Automated Reasoning Kit. SNARK...
  • DISCOUNT

  • Referenced in 7 articles [sw19613]
  • A distributed and learning equational prover DISCOUNT. The...
  • HOL88

  • Referenced in 1 article [sw19615]
  • The HOL System is an environment for interactive...
  • HOL90

  • Referenced in 4 articles [sw19616]
  • HOL90: The rational reconstruction of HOL88....
  • PRV

  • Referenced in 1 article [sw19617]
  • PRV-Beweisprogramm: An early theorem prover written in...
  • CLIN

  • Referenced in 5 articles [sw19618]
  • A semantically guided first-order theorem prover CLIN...