• Maude-NPA

  • Referenced in 29 articles [sw12159]
  • reasoning about the security of cryptographic protocols in which the cryptosystems satisfy different equational properties ... original NRL Protocol Analyzer, which supported equational reasoning in a more limited way. Maude ... sessions and the support for different equational theories, it is necessary to develop ways...
  • RRL

  • Referenced in 55 articles [sw28904]
  • environment for experimenting with automated reasoning algorithms for equational logic based on rewrite techniques ... hard and challenging mathematical problems in automated reasoning literature as well as a research tool...
  • Nominal Isabelle

  • Referenced in 72 articles [sw12055]
  • equivalence and establishes automatically the reasoning infrastructure for α-equated terms. We also prove strong...
  • TAMARIN

  • Referenced in 15 articles [sw23438]
  • support for efficient deduction and equational reasoning. We provide an overview of the tool...
  • EQP

  • Referenced in 12 articles [sw15620]
  • matching, a variety of strategies for equational reasoning, and fast search. It seems to perform...
  • iProver-Eq

  • Referenced in 8 articles [sw09452]
  • iProver system with superposition-based equational reasoning and maintains the distinctive features of the Inst ... solver. The first-order reasoning employs a saturation algorithm making use of redundancy elimination ... simplification inferences. We describe the equational reasoning as it is implemented in iProver...
  • UG

  • Referenced in 190 articles [sw04596]
  • numerical solution of partial differential equations have been developed. We are especially interested in adaptive ... commercial codes use them. There are two reasons for this. Firstly, the multigrid solution...
  • TENSOLVE

  • Referenced in 28 articles [sw00956]
  • equations and unknowns, in cases where it is reasonable to calculate the Jacobian matrix...
  • UTP2

  • Referenced in 5 articles [sw06342]
  • support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that...
  • Saoithin

  • Referenced in 4 articles [sw06341]
  • support the higher-order logic, alphabets, equational reasoning and “programs as predicates” style that...
  • FMMLIB2D

  • Referenced in 29 articles [sw12486]
  • Helmholtz equation in free space. The codes are easy to use and reasonably well optimized...
  • StrSolve

  • Referenced in 5 articles [sw21857]
  • present StrSolve, a decision procedure that reasons about equations over string variables. Our approach scales...
  • MadMax

  • Referenced in 2 articles [sw28631]
  • maximal ordered completion tool. The equational reasoning tool MædMax implements maximal ordered completion. This ... Hirokawa (2011) to ordered completion and equational theorem proving. MædMax incorporates powerful ground completeness checks...
  • 4D-VAR

  • Referenced in 13 articles [sw03477]
  • simplicity reasons, as it does not require any linearization, or adjoint equation, or minimization process...
  • Java+ITP

  • Referenced in 8 articles [sw32259]
  • fragment as an equational theory in Maude. It supports compositional reasoning in a Hoare logic...
  • Applicative Lifting

  • Referenced in 1 article [sw28587]
  • types, as observed by Hinze. Thus, equational reasoning over effectful computations can be reduced ... proof methods for lifting of equations over applicative functors. The first method normalises applicative expressions...
  • Metatheory.jl

  • Referenced in 1 article [sw37953]
  • between symbolic mathematics, abstract interpretation, equational reasoning, optimization, composable compiler transforms, and advanced homoiconic pattern...
  • TRICE

  • Referenced in 46 articles [sw05197]
  • linearized state equation and the adjoint equation. They are well suited for large scale problems ... mild conditions on the trial steps. Under reasonable, but more stringent, conditions on the quadratic ... control problem governed by a nonlinear heat equation are reported...
  • YAPA

  • Referenced in 19 articles [sw02739]
  • generic tool for computing intruder knowledge. Reasoning about the knowledge of an attacker ... calculus, as in similar languages based on equational logics, knowledge is typically expressed...
  • cheney-kincaid

  • Referenced in 25 articles [sw11656]
  • have been reordered for logical and pedagogical reasons. The discussion of floating-point number representation ... chapter on solving linear systems of equations. A new appendix on the concepts and notation...