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

DOI10.1016/0167-6423(87)90004-9MaRDI QIDQ1097686zbMATH OpenOpenAlexFDO

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

zbMATH Keywords

built-in theoriescompletion procedureREVEUR-3strategiesterm rewriting systems

Mathematics Subject Classification ID

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

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

Cited in

(5)

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

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)