Testing for the ground (co-)reducibility property in term-rewriting systems

DOI10.1016/0304-3975(92)90279-OMaRDI QIDQ685352zbMATHFDO

Authors Emmanuel Kounalis

Publication date 25 October 1993

Published in Theoretical Computer Science (Search for Journal in Brave)

zbMATH Keywords

Knuth-Bendix completionarbitrary term-rewriting systemsground-co-reducibleground-reduciblemechanizing inductive proofs

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42)

Recommendations

• scientific article; zbMATH DE number 125892
• scientific article; zbMATH DE number 58292
• Computing ground reducibility and inductively complete positions
• Towards an efficient construction of test sets for deciding ground reducibility
• Term rewriting restricted to ground terms.

Cites work

• scientific article; zbMATH DE number 4164140 (Why is no real title available?)
• scientific article; zbMATH DE number 4164142 (Why is no real title available?)
• scientific article; zbMATH DE number 3943001 (Why is no real title available?)
• scientific article; zbMATH DE number 3956434 (Why is no real title available?)
• scientific article; zbMATH DE number 4037157 (Why is no real title available?)
• scientific article; zbMATH DE number 4043234 (Why is no real title available?)
• scientific article; zbMATH DE number 3664335 (Why is no real title available?)
• scientific article; zbMATH DE number 18637 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• Automatic proofs by induction in theories without constructors
• Computing ground reducibility and inductively complete positions
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• On sufficient-completeness and related properties of term rewriting systems
• Proofs by induction in equational theories with constructors
• Semantic confluence tests and completion methods

Cited in

(11)

• Ground reducibility is EXPTIME-complete
• Using induction and rewriting to verify and complete parameterized specifications
• Proving weak properties of rewriting
• Computing ground reducibility and inductively complete positions
• Test sets for the universal and existential closure of regular tree languages.
• scientific article; zbMATH DE number 1765706 (Why is no real title available?)
• Towards an efficient construction of test sets for deciding ground reducibility
• scientific article; zbMATH DE number 125892 (Why is no real title available?)
• Mechanizable inductive proofs for a class of \(\forall \exists\) formulas
• Pumping, cleaning and symbolic constraints solving
• Observational proofs by rewriting.

This page was built for publication: Testing for the ground (co-)reducibility property in term-rewriting systems

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