• OTTER

  • Referenced in 316 articles [sw02904]
  • current automated deduction system Otter is designed to prove theorems stated in first-order logic...
  • MaLARea

  • Referenced in 46 articles [sw10278]
  • simple metasystem iteratively combining deductive Automated Reasoning tools (now the E and the SPASS...
  • ETPS

  • Referenced in 157 articles [sw06302]
  • proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems...
  • SAD

  • Referenced in 14 articles [sw09796]
  • System for automated deduction (SAD): A tool for proof verification. In this paper a proof...
  • Why3

  • Referenced in 131 articles [sw04438]
  • Why3 is a platform for deductive program verification. It provides a rich language for specification ... relies on external theorem provers, both automated and interactive, to discharge verification conditions. Why3 comes...
  • GAPT

  • Referenced in 9 articles [sw22200]
  • components common in proof theory and automated deduction. In contrast to automated and interactive theorem...
  • TPS

  • Referenced in 71 articles [sw00973]
  • proving include hardware and software verification, partial automation of various mathematical activities, promoting development ... theories in a wide variety of disciplines, deductive information systems for these disciplines, expert systems...
  • HERBY

  • Referenced in 6 articles [sw21545]
  • have participated in the Conference on Automated Deduction’s competitions. The sourse cod has evolved...
  • mkbTT

  • Referenced in 6 articles [sw10018]
  • completion is a classical calculus in automated deduction for transforming a set of equations into...
  • KeYmaera

  • Referenced in 41 articles [sw03709]
  • combines deductive, real algebraic, and computer algebraic prover technologies. It is an automated and interactive...
  • TRAMP

  • Referenced in 21 articles [sw21343]
  • several automated theorem provers for first order logic with equality into natural deduction proofs...
  • F*

  • Referenced in 20 articles [sw27563]
  • puts together the automation of an SMT-backed deductive verification tool with the expressive power...
  • daTac

  • Referenced in 3 articles [sw26325]
  • system daTac is to do automated deduction in first-order logic with equality. Its speciality...
  • GEX

  • Referenced in 35 articles [sw09961]
  • learning of various mathematical concepts. As an automated reasoning software, we can build dynamic logic ... past twenty years, including the deductive base method, Wu’s method, the area method ... angle method. With these methods, users may automated prove geometry theorems, to discover new prrperties...
  • dedukti

  • Referenced in 19 articles [sw13663]
  • Deduction Modulo: G. Dowek, Th. Hardin, C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning...
  • Grail

  • Referenced in 7 articles [sw24229]
  • fragments for categorial logics. Grail is an automated theorem prover based on proof nets ... graph-based representation of proofs, and labeled deduction...
  • CardKt

  • Referenced in 1 article [sw01599]
  • CardKt: Automated multi-modal deduction on Java cards for multi-application security. We describe ... Java program to perform automated deduction in propositional multi-modal logics on a Java smart...
  • KEIM

  • Referenced in 1 article [sw19608]
  • KEIM: A toolkit for automated deduction. KEIM is a collection of software modules, written ... used in the implementation of automated reasoning systems. KEIM is intended to be used ... those who want to build or use deduction systems (such as resolution theorem provers) without...
  • ANDP

  • Referenced in 1 article [sw29686]
  • Automated natural deduction prover and experiments. The paper presents the heuristics and techniques which ... used to implement automated natural deduction prover (ANDP), the natural deduction was adapted from Gentzen...
  • TAMARIN

  • Referenced in 15 articles [sw23438]
  • security protocols. The Tamarin prover supports the automated, unbounded, symbolic analysis of security protocols ... models, and properties, and support for efficient deduction and equational reasoning. We provide an overview...