
RRtools
 Referenced in 33 articles
[sw00814]
 aiding the discovery and proof of finite RogersRamanujan type identities...

recpf
 Referenced in 26 articles
[sw06642]
 assist in the discovery and proof of finitizations of identities of the RogersRamanujan 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 computerassisted 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...

EnKFMC
 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 ThetaFunction Identities. This is a tutorial for using two new MAPLE...

thetaids
 Referenced in 1 article
[sw28289]
 Automatic Proof of ThetaFunction 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 proofcarrying 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...