Correctness of Context-Moving Transformations for Term Rewriting Systems

DOI10.1007/978-3-319-27436-2_20MaRDI QIDQ5743602zbMATH OpenOpenAlexFDO

Authors Koichi Sato, Kentaro Kikuchi, Takahito Aoto, Yoshihito Toyama

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

inductive theorem provingprogram transformationtail-recursionterm-rewriting system

Mathematics Subject Classification ID

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

Recommendations

• scientific article; zbMATH DE number 3949707
• Correctness of program transformations as a termination problem
• Proving termination of context-sensitive rewriting by transformation
• scientific article; zbMATH DE number 1722708
• Transformations of Conditional Rewrite Systems Revisited
• Transformation for refining unraveled conditional term rewriting systems
• Transformation techniques for context-sensitive rewrite systems
• Remarks on Thatte's transformation of term rewriting systems
• Correctness of high-level transformation systems relative to nested conditions
• A compact fixpoint semantics for term rewriting systems

Cites work

• A general framework to build contextual cover set induction provers
• Automated Mathematical Induction
• scientific article; zbMATH DE number 1615264 (Why is no real title available?)
• scientific article; zbMATH DE number 1149426 (Why is no real title available?)
• Induction proofs with partial functions
• On sufficient-completeness and related properties of term rewriting systems
• Sound generalizations in mathematical induction
• Sound lemma generation for proving inductive validity of equations

Cited in

(2)

• Conversion to tail recursion in term rewriting
• scientific article; zbMATH DE number 1615264 (Why is no real title available?)

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

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