
MTT
 Referenced in 24 articles
[sw09783]
 development of the theory of termination of rewriting, its application to highlevel programming languages ... equations and rules, types and subtypes, (possibly programmable) strategies for controlling the execution, matching modulo ... inference system rather than just by a rewriting relation. In particular, Generalized Rewrite Theories...

ChC 3
 Referenced in 11 articles
[sw09781]
 rewrite theory to be executable, its equations E should be (ground) confluent and terminating modulo ... rules should be (ground) coherent with E modulo A. The correctness of many important formal ... many specifications of interest are typed, have equations E and rules R that are both ... ground coherence checking for ordersorted rewrite theories under these general assumptions. We also explain...

CRC 3
 Referenced in 9 articles
[sw09782]
 mathematical semantics, and its operational semantics by rewriting. Checking this property for expressive specifications that ... their condition, and whose equations can be applied modulo different combinations of associativity, commutativity...

daTac
 Referenced in 3 articles
[sw26325]
 speciality is to apply deductions modulo some equational properties of operators, such as commutativity ... implemented, based on resolution, paramodulation and term rewriting, have been proved refutationally complete in [RV95...

Coq
 Referenced in 1880 articles
[sw00161]
 Coq is a formal proof management system. It...

GAP
 Referenced in 3154 articles
[sw00320]
 GAP is a system for computational discrete algebra...

Isabelle
 Referenced in 698 articles
[sw00454]
 Isabelle is a generic proof assistant. It allows...

Magma
 Referenced in 3296 articles
[sw00540]
 Computer algebra system (CAS). Magma is a large...

Maple
 Referenced in 5363 articles
[sw00545]
 The result of over 30 years of cutting...

Mathematica
 Referenced in 6337 articles
[sw00554]
 Almost any workflow involves computing results, and that...

MiniSat
 Referenced in 565 articles
[sw00577]
 An extensible SATsolver. MiniSat is a minimalistic...

nauty
 Referenced in 609 articles
[sw00611]
 graphtheoretic program NAUTY: nauty is a program...

REDUCE
 Referenced in 746 articles
[sw00789]
 REDUCE is an interactive system for general algebraic...

SageMath
 Referenced in 1970 articles
[sw00825]
 Sage (SageMath) is free, opensource math software...

Theorema
 Referenced in 149 articles
[sw00961]
 The software system Theorema provides a uniform logic...

TPS
 Referenced in 73 articles
[sw00973]
 TPS and ETPS are, respectively, the Theorem Proving...

PRISM
 Referenced in 442 articles
[sw01186]
 PRISM: Probabilistic symbolic model checker. In this paper...

MACSYMA
 Referenced in 720 articles
[sw01209]
 Macsyma is a general purpose symbolicnumericalgraphical...

Modula
 Referenced in 197 articles
[sw01224]
 The Modula programming language is a descendant of...