• TPA

  • Referenced in 13 articles [sw10114]
  • latter, TPA is capable of delivering automated termination proofs for some difficult TRSs for which...
  • Jakarta

  • Referenced in 18 articles [sw01269]
  • that translates JSL specifications into proof assistants; the JaKarTa Automation Kit (JAK), a toolset...
  • HOL-Boogie

  • Referenced in 14 articles [sw00409]
  • from these annotations -- are usually transferred to automated theorem provers such as Simplify ... this paper, however, we present a proof-environment, HOL-BoogieP, that combines Boogie with ... present specific techniques combining automated and interactive proof methods for code-verification.\parWe will exploit...
  • SEPIA

  • Referenced in 7 articles [sw21585]
  • paper describes SEPIA, a tool for automated proof generation in Coq. SEPIA combines model inference ... then be traversed automatically to identify proofs. The SEPIA system is described and its performance ... SEPIA provides a useful complement to existing automated tactics...
  • Eisbach

  • Referenced in 7 articles [sw13077]
  • Isabelle proof method language. Machine-checked proofs are becoming ever-larger, presenting an increasing maintenance ... previously lacked a means to write automated proof procedures. This can lead to more duplication...
  • Hipster

  • Referenced in 7 articles [sw11223]
  • proof mode complements and boosts existing proof automation techniques that rely on automatically selecting existing...
  • CoqHammer

  • Referenced in 15 articles [sw29396]
  • purpose automated reasoning hammer tool for Coq. It combines learning from previous proofs with ... logics of automated systems and the reconstruction of successfully found proofs. A typical...
  • GAPT

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

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

  • Referenced in 4 articles [sw28627]
  • translation to automated reasoning have recently become an important component of formal proof assistants ... Such ”hammer” tech- niques complement traditional proof assistant automation as implemented by tactics and decision ... this paper we present a unified proof assistant automation approach which attempts to automate ... implement the technique as a tactic-level automation for HOL4: TacticToe. It implements a modified...
  • KeYmaera

  • Referenced in 42 articles [sw03709]
  • automating the verification process, KeYmaera implements a generalized free-variable sequent calculus and automatic proof...
  • Coquelicot

  • Referenced in 12 articles [sw11552]
  • help with the proof process, the library comes with a comprehensive set of theorems that ... behaviors. It also offers some automation for performing differentiability proofs. Moreover, Coquelicot is a conservative...
  • GEX

  • Referenced in 35 articles [sw09961]
  • automated prove geometry theorems, to discover new prrperties of theorems, and to generate readable proofs...
  • miz3

  • Referenced in 11 articles [sw18631]
  • procedural style – strong automation and help with shaping the proofs, including determining the statements...
  • Tecton

  • Referenced in 9 articles [sw28905]
  • internally in a structured form called a proof forest; displaying them in an easy ... representations, and hypertext links; and automating substantial parts of proofs through rewriting, induction, case analysis...
  • IsaFoR

  • Referenced in 5 articles [sw10106]
  • rewriting. We show how to automate termination proofs for recursive functions in (a first-order ... challenge is the formal reduction of the proof obligation produced by Isabelle/HOL to the termination ... corresponding term rewrite system. We automate this reduction via suitable tactics which we added...
  • Lean

  • Referenced in 39 articles [sw15148]
  • interactive and automated theorem proving, by situating automated tools and methods in a framework that ... construction of fully specified axiomatic proofs. Lean is an ongoing and long-term effort...
  • SAD

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

  • Referenced in 19 articles [sw13663]
  • typed rewrite rules, capable of expressing proofs in Deduction Modulo: G. Dowek, Th. Hardin ... Kirchner, Theorem proving modulo, Journal of Automated Reasoning...
  • HOLCF

  • Referenced in 3 articles [sw25266]
  • while providing a high degree of proof automation. The soundness of the system is ensured ... such a model in a formal proof tool...