AProVE -
a tool for automated termination and innermost termination proofs of
(conditional) term rewrite systems (TRSs). AProVE offers the techniques
of polynomial orders, recursive path orders possibly with status,
dependency pairs including recent refinements such as narrowing,
rewriting, and (forward-)instantiation of dependency pairs, and the
size-change principle, also in combination with dependency pairs. The
tool is written in Java and proofs can be performed both in a fully
automated or in an interactive mode via a graphical user interface.
Contact:
AProVE Group
<aprove @ i2.informatik.rwth-aachen.de>
ASF+SDF -
an algebraic specification formalism for developing language
definitions, both syntax and semantics. The ASF+SDF Meta-Environment is
an integrated programming environment to develop ASF+SDF specifications
and to generate environments for the developed specifications.
CiME -
a tool for checking termination and confluence of rewrite
systems modulo equational theories, and for completion of such
systems. Includes the Normalized completion algorithm
and the dependency pairs criterion for termination. Also
provides unification algorithms modulo Associativity and
Commutativity, Abelian Groups and Boolean Rings.
CoLoR -
a Coq Library on Rewriting and termination.
Coq is a proof assistant developped at INRIA available at
http://coq.inria.fr/. The aim of this Coq library is to provide the
necessary formal basis for certifying the termination witnesses searched
and built by termination tools like CiME, AProVE, TTT, Cariboo, etc.
ELAN -
an environment to prototype the combination of different
computational systems that provide a basis for constraint
solving, theorem proving and logic programming paradigms.
LP (the Larch Prover) -
a first order prover designed for a middle ground between
proof checkers that require detailed guidance and theorem
provers that work completely automatically.
Maude -
a high-performance multiparadigm language based on rewriting logic, and
contains a functional sublanguage based on equational logic. It can be
used for both programming and executable system specification in a
variety of areas such as distributed and mobile systems and
communication protocols, and functional applications. Thanks to its
reflective features it can be used as a metalanguage and is easily
extensible with powerful module composition operations as those
supported in its Full Maude extension. It can also be used as a
semantic framework to specify and prototype different languages,
concurrency calculi, and SOS specifications; and as a logical framework
to represent and mechanize different logics and proving tools.
MU-TERM -
a Tool for Proving Termination of Rewriting with Replacement
Restrictions.
The tool implements the generation of orderings for proving termination
of Context-Sensitive Rewriting (CSR). Proofs of termination of CSR are
also possible via existing transformations to TRSs which are also
implemented in MU-TERM. These techniques can also be used, in a number
of different ways, for proving termination of ordinary rewriting and
other restrictions of rewriting.
OBJ3 -
a language based on order sorted equational logic, that has
been successfully used for research and teaching in software
design and specification, rapid prototyping, theorem proving,
user interface design, and hardware verification, among other
things. It was the first language to implement parameterized
programming.
OSHL -
an instance-based first-order theorem prover that can use
natural semantics to guide its search. It is based on a
strategy called ordered semantic hyper linking. It has
term-rewriting facilities built in as well as special
techniques for AC symbols, but not AC unification, and special
techniques for set theory. It is also propositionally
efficient and goal-sensitive.
RRL (Rewrite Rule Laboratory) -
a rewrite-rule based theorem prover for equational and
inductive reasoning. Recently the theorem prover has been used
for hardware verification application.
TOM -
a pattern matching compiler developed at INRIA. It is particularly
well-suited for programming various transformations on trees/terms and
XML based documents. Its design follows our research on rule based
languages (R3), and our experiences on the efficient compilation of ELAN
developed by the Protheo group.an environment to prototype the
combination of different computational systems that provide a basis for
constraint solving, theorem proving and logic programming paradigms.
Watson (formerly Mark2) -
an interactive equational theorem prover, where theorems are rewrite
rules, with a programming language (programs are systems of recursively
chained rewrite rules, proved and stored in the same way as theorems),
and with dedicated features for reasoning about expressions defined by
cases and supporting a higher-order logic with the strength of type
theory.