• Nominal Isabelle

• Referenced in 76 articles [sw12055]
• equivalence in Nominal Isabelle. Nominal Isabelle is a definitional extension of the Isabelle/HOL theorem prover ... extension includes new definitions of α-equivalence and establishes automatically the reasoning infrastructure...

• QuantumMACMAHON

• Referenced in 21 articles [sw11441]
• Zeilberger: The MacMahon’s Master Theorem relates a certain generating function obtained from a square ... determinant of I-A. An equivalent formulation of this theorem is the boson-fermion correspondence...

• KRIPKE

• Referenced in 8 articles [sw01162]
• shown in [8] to be equivalent to the numbertheoretic theorem was shown ... equivalent to the number-theoretic theorem known as Dickson’s theorem (for details of which...

• designv2

• Referenced in 3 articles [sw27807]
• also evaluates these designs using General Equivalence Theorem results. A related article...

• Ctrl

• Referenced in 7 articles [sw13874]
• manual and automatic mode for equivalence tests using inductive theorem proving, giving support...

• ICAOD

• Referenced in 2 articles [sw16271]
• with respect to different criteria by equivalence theorem. ICA is a meta-heuristic evolutionary algorithm...

• SAGEMoLiC

• Referenced in 1 article [sw29863]
• previous systems, our approach to visualize equivalence theorems is not a simple “step by step ... involved in the formal proofs of these equivalences...

• Hotel Key Card

• Referenced in 3 articles [sw29234]
• defined, verified, and proved equivalent in the theorem prover Isabelle/HOL. It is shown that...

• KAT-ML

• Referenced in 10 articles [sw08506]
• implementation of an interactive theorem prover for Kleene algebra with tests (KAT). The system ... with some examples, including an extensive scheme equivalence proof...

• CAV

• Referenced in 12 articles [sw06910]
• theorem giving a sufficient condition for when two pattern sets are strongly (consecutively) Wilf-equivalent...

• TVOC

• Referenced in 20 articles [sw02521]
• given source program, TVOC proves the equivalence of the source code and the target code ... Verification conditions are validated using the automatic theorem prover CVC Lite...

• SQEMA

• Referenced in 40 articles [sw03056]
• algorithm SQEMA for computing first-order equivalents and proving canonicity of modal formulae, and thus ... special modal version of Lyndon’s monotonicity theorem and imposing additional requirements on the Ackermann...

• Java+ITP

• Referenced in 8 articles [sw32259]
• equivalent first-order verification conditions (VCs) which are then sent to Maude’s Inductive Theorem...

• Regex_Equivalence

• Referenced in 7 articles [sw32229]
• verified decision procedures for regular expression equivalence. Five recently published formalizations of such decision procedures ... same name presented at Interactive Theorem Proving...

• AREP

• Referenced in 9 articles [sw13167]
• representations are considered and manipulated, rather than equivalence classes of representations as it is done ... characters. Thus, we present well-known theorems in a constructively refined form and derive...

• Beaver

• Referenced in 10 articles [sw00071]
• vector arithmetic. Beaver is an SMT solver (theorem prover) for the theory of quantifier-free ... queries), security (rich in nonlinear arithmetic) and equivalence checking (rich Boolean structure...

• PySRURGS

• Referenced in 2 articles [sw32436]
• Free Lunch Theorem argues that random search should be equivalent to other approaches like Genetic...

• BRAID

• Referenced in 18 articles [sw04311]
• finite group. By Riemann’s existence theorem, braid orbits of generating systems for G with ... describe the various possibilities up to equivalence of covers. They also consider the case...

• GenerateUHG

• Referenced in 5 articles [sw26974]
• This gives the strongest form of a theorem of Entringer and Swart, and sheds light ... Fleischner originally settled by Seamone. We prove equivalent formulations of the conjecture of Bondy...

• PREVAIL

• Referenced in 7 articles [sw02114]
• formal verification environment for proving the equivalence of two VHDL architectures of the same design ... according to pre-defined templates, and a theorem is generated in a form acceptable...