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

DOI10.1016/0304-3975(92)90279-OzbMath0776.68069MaRDI QIDQ685352

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)

Related Items

Ground reducibility is EXPTIME-complete, Towards an efficient construction of test sets for deciding ground reducibility, Test sets for the universal and existential closure of regular tree languages., Pumping, cleaning and symbolic constraints solving, Using induction and rewriting to verify and complete parameterized specifications, Proving weak properties of rewriting, Mechanizable inductive proofs for a class of ∀ ∃ formulas, Observational proofs by rewriting.

Cites Work

• Proofs by induction in equational theories with constructors
• On sufficient-completeness and related properties of term rewriting systems
• Automatic proofs by induction in theories without constructors
• Semantic confluence tests and completion methods
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• Computing ground reducibility and inductively complete positions
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item