REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies

DOI10.1016/0167-6423(87)90004-9zbMATH Open0635.68017OpenAlexW1985706915MaRDI QIDQ1097686FDOQ1097686

Authors: Claude Kirchner, Hélène Kirchner 

Publication date: 1987

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0167-6423(87)90004-9

Recommendations

• scientific article; zbMATH DE number 3896335
• scientific article; zbMATH DE number 3871335
• scientific article; zbMATH DE number 4092744
• Termination by completion
• Some experiments with a completion theorem prover

zbMATH Keywords

term rewriting systemsstrategiescompletion procedurebuilt-in theoriesREVEUR-3

Mathematics Subject Classification ID

General topics in the theory of software (68N01) Abstract data types; algebraic specification (68Q65)

Cited In (5)

• Rewriting with a nondeterministic choice operator
• Unification in combinations of collapse-free regular theories
• Automatic proofs by induction in theories without constructors
• Equational completion in order-sorted algebras
• Computations in APS

This page was built for publication: REVEUR-3: The implementation of a general completion procedure parameterized by built-in theories and strategies

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1097686)