• RRtools

  • Referenced in 33 articles [sw00814]
  • aiding the discovery and proof of finite Rogers-Ramanujan type identities...
  • recpf

  • Referenced in 26 articles [sw06642]
  • assist in the discovery and proof of finitizations of identities of the Rogers-Ramanujan type...
  • StanBij.mws

  • Referenced in 10 articles [sw06645]
  • combinatorial proof of a partition identity of Andrews and Stanley In his paper ... certain partition identity analytically and asks for a combinatorial proof. This paper provides the requested...
  • MultInt

  • Referenced in 6 articles [sw00603]
  • MultInt can be used to generate proofs of identities (or recurrences) involving multiple integrals...
  • HYPERG

  • Referenced in 5 articles [sw00423]
  • This package provides tools for automatic proofs of identities; transforming sums into hypergeometric notation; manipulating...
  • Tame Graphs

  • Referenced in 16 articles [sw28578]
  • Proofs. [CUP 2012]. The values of the constants in the definition of tameness are identical ... refers to the original version of Hales’ proof, the ITP 2011 paper by Nipkow refers...
  • BijTools

  • Referenced in 3 articles [sw12643]
  • finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
  • Examples

  • Referenced in 3 articles [sw12644]
  • finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
  • Fibonacci

  • Referenced in 3 articles [sw12645]
  • finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
  • TransMethodZeck

  • Referenced in 3 articles [sw12646]
  • finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
  • ZeckFibBijections

  • Referenced in 3 articles [sw12647]
  • finding combinatorial bijections. Consider a combinatorial identity that can be proved by induction. In this ... general method for translating the inductive proof into a recursive bijection. Furthermore, we will demonstrate ... often results in a bijective proof of the identity that helps illuminate the underlying combinatorial...
  • RComp

  • Referenced in 5 articles [sw00785]
  • large class of identities involving these sequences computer generated proofs can be obtained...
  • OrientedSwaps

  • Referenced in 2 articles [sw35044]
  • Knuth and Burge correspondences. A second probabilistic identity, relating those two vectors to a vector ... give a computer-assisted proof of this identity for n≤6 after first reformulating...
  • MJ

  • Referenced in 12 articles [sw24342]
  • which are sufficiently small to facilitate formal proofs of key properties. However many ... compact, MJ models features such as object identity, field assignment, constructor methods and block structure ... operational semantics of MJ, and give a proof of type safety. In order to demonstrate...
  • EnKF-MC

  • Referenced in 4 articles [sw15209]
  • based on various matrix identities are provided. Furthermore, an asymptotic proof of convergence with regard...
  • ramarobinsids

  • Referenced in 1 article [sw28288]
  • Automatic Proof of Theta-Function Identities. This is a tutorial for using two new MAPLE...
  • thetaids

  • Referenced in 1 article [sw28289]
  • Automatic Proof of Theta-Function Identities. This is a tutorial for using two new MAPLE...
  • Grail

  • Referenced in 5 articles [sw26751]
  • dual identity in the Mobile Resource Guarantees project, where Grail serves as proof-carrying code...
  • Regular_Algebras

  • Referenced in 3 articles [sw32237]
  • regular expressions as induced by regular language identity. We use Isabelle/HOL for a detailed systematic ... relationships between these classes, formalise a soundness proof for the smallest class (Salomaa ... provide a large collection of regular identities in the general setting of Boffa’s axiom ... algebra hierarchy in the Archive of Formal Proofs; we have not aimed at an integration...
  • SicoTHEO

  • Referenced in 8 articles [sw09982]
  • exploited by competition: on each processor, an identical copy of SETHEO tries to prove ... soon as one processor finds a proof, the entire system is stopped. Three different versions...