
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 IA. An equivalent formulation of this theorem is the bosonfermion correspondence...

KRIPKE
 Referenced in 8 articles
[sw01162]
 shown in [8] to be equivalent to the numbertheoretic theorem was shown ... equivalent to the numbertheoretic 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 metaheuristic 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...

KATML
 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) Wilfequivalent...

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 firstorder 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 firstorder 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 wellknown 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 quantifierfree ... 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 predefined templates, and a theorem is generated in a form acceptable...