×

REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies. (English) Zbl 0635.68017

Summary: This paper describes REVEUR-3, a software that implements a general completion procedure, REVEUR-3 allows working with built-in theories and strategies and is aimed to perform proofs and experiments in term rewriting systems. These features are illustrated by experimental results.

MSC:

68Q65 Abstract data types; algebraic specification
68N01 General topics in the theory of software
PDFBibTeX XMLCite
Full Text: DOI