
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 firstorder 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 KnuthBendix 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]
 highspeed 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 semiautomatic 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 firstorder logic with equality. Otter’s inference rules are based ... symbolic calculator and has an embedded equational programming system. Otter is a fourthgeneration 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 firstorder 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 ... hiddensorted semantics.par Maude’s underlying equational logic, membership equational logic, generalizes and increases ... manysorted and ordersorted equational logics. We develop a hiddensorted extension of membership ... equational logic, and give conditions under which theories have both an algebraic and a coalgebraic...

Kiva2
 Referenced in 66 articles
[sw08987]
 easeofuse. The KIVA2 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...

Peersmcd
 Referenced in 3 articles
[sw23958]
 implements contractionbased strategies for equational logic, modulo associativity and commutativity, with paramodulation, simplification...

UTP2
 Referenced in 5 articles
[sw06342]
 support the higherorder 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 higherorder logic, alphabets, equational reasoning and “programs as predicates” style that...