• 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...