Correctness of Context-Moving Transformations for Term Rewriting Systems

DOI10.1007/978-3-319-27436-2_20zbMath1473.68057OpenAlexW2408365838MaRDI QIDQ5743602

Yoshihito Toyama, Kentaro Kikuchi, Koichi Sato, Takahito Aoto

Publication date: 5 February 2016

Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-27436-2_20

zbMATH Keywords

program transformationinductive theorem provingterm-rewriting systemtail-recursion

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Grammars and rewriting systems (68Q42) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• Unnamed Item
• Unnamed Item
• On sufficient-completeness and related properties of term rewriting systems
• Induction proofs with partial functions
• Sound generalizations in mathematical induction
• Sound lemma generation for proving inductive validity of equations
• Automated Mathematical Induction
• A general framework to build contextual cover set induction provers

This page was built for publication: Correctness of Context-Moving Transformations for Term Rewriting Systems