• Maude

  • Referenced in 698 articles [sw06233]
  • language and system supporting both equational and rewriting logic specification and programming for a wide ... which can be regarded as an equational logic sublanguage. Besides supporting equational specification and programming...
  • Prover9

  • Referenced in 197 articles [sw04969]
  • theorem prover for first-order and equational logic, and Mace4 searches for finite models...
  • OBJ3

  • Referenced in 140 articles [sw05370]
  • proof system based on order sorted equational logic. It has been successfully used for research...
  • RRL

  • Referenced in 55 articles [sw28904]
  • experimenting with automated reasoning algorithms for equational logic based on rewrite techniques...
  • Waldmeister

  • Referenced in 46 articles [sw19568]
  • theorem prover for unit equational logic. Its proof procedure is unfailing Knuth-Bendix completion [BDP89...
  • ITP

  • Referenced in 31 articles [sw09808]
  • support incremental development of specifications. Membership equational logic is an expressive version of equational logic...
  • JPAX

  • Referenced in 29 articles [sw09906]
  • high-speed rewriting system for equational logic, but here extended with executable temporal logic...
  • DDebugger

  • Referenced in 15 articles [sw09904]
  • Declarative debugging of rewriting logic specifications. Declarative debugging is a semi-automatic technique that starts ... find the error. Membership equational logic (MEL) is an equational logic that in addition ... equations allows one to state membership axioms characterizing the elements of a sort. Rewriting logic ... least sorts with the equational subset of rewriting logic, and rewrites and sets of reachable...
  • OTTER

  • Referenced in 316 articles [sw02904]
  • prove theorems stated in first-order logic with equality. Otter’s inference rules are based ... symbolic calculator and has an embedded equational programming system. Otter is a fourth-generation Argonne ... research in abstract algebra and formal logic. Otter and its predecessors have been used...
  • YAPA

  • Referenced in 19 articles [sw02739]
  • similar languages based on equational logics, knowledge is typically expressed by two relations: deducibility ... these relations under a variety of equational theories. However, each theory has its particular algorithm...
  • EQP

  • Referenced in 12 articles [sw15620]
  • theorem proving program for first-order equational logic. Its strengths are good implementations of associative ... matching, a variety of strategies for equational reasoning, and fast search. It seems to perform...
  • AMRCLAW

  • Referenced in 68 articles [sw15478]
  • variety of new problems, including hyperbolic equations, which are not in a conservation form, problems ... with source terms of capacity functions, and logically rectangular curvilinear grids. The developed framework requires...
  • Kumo

  • Referenced in 5 articles [sw06963]
  • first order logic and hidden equational logic are implemented, including induction and coinduction. Kumo generates...
  • BMaude

  • Referenced in 2 articles [sw10135]
  • Towards behavioral Maude: behavioral membership equational logic. How can algebraic and coalgebraic specifications be integrated ... hidden-sorted semantics.par Maude’s underlying equational logic, membership equational logic, generalizes and increases ... many-sorted and order-sorted equational logics. We develop a hidden-sorted extension of membership ... equational logic, and give conditions under which theories have both an algebraic and a coalgebraic...
  • Kiva-2

  • Referenced in 66 articles [sw08987]
  • ease-of-use. The KIVA-2 equations and numerical solution procedures are very general ... written for internal combustion engine calculations, the logic for these specifications can be easily modified ... program, we describe in detail the equations solved, the numerical solution procedure, and the structure...
  • KBCV

  • Referenced in 3 articles [sw19459]
  • generation of (dis)proofs in equational logic is supported. Finally, the tool outputs proofs...
  • Peers-mcd

  • Referenced in 3 articles [sw23958]
  • implements contraction-based strategies for equational logic, modulo associativity and commutativity, with paramodulation, simplification...
  • UTP2

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

  • Referenced in 22 articles [sw20123]
  • differential equations and automata and a specification in a fragment of Linear Temporal Logic that...
  • Saoithin

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