Transforming orthogonal inductive definition sets into confluent term rewrite systems

DOI10.1016/j.jlamp.2022.100779OpenAlexW4229038222MaRDI QIDQ2141298

Naoki Nishida, Shujun Zhang

Publication date: 25 May 2022

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2022.100779

zbMATH Keywords

first-order logicprogram transformationterminationterm rewritingdependency pairinductive theorem

Mathematics Subject Classification ID

Computer science (68-XX)

Uses Software

• Tyrolean
• Cyclist

Cites Work

• Unnamed Item
• Unnamed Item
• Tools for proving inductive equalities, relative completeness, and \(\omega\)-completeness
• Proofs and algorithms. An introduction to logic and computability
• Tyrolean termination tool: techniques and features
• Modular termination proofs for rewriting using dependency pairs
• Operational semantics of resolution and productivity in Horn clause logic
• Term Rewriting with Logical Constraints
• Automated termination proofs for logic programs by term rewriting
• Automated Termination Analysis for Logic Programs by Term Rewriting
• Verifying Procedural Programs via Constrained Rewriting Induction
• AC Dependency Pairs Revisited
• Automated Reasoning with Analytic Tableaux and Related Methods

This page was built for publication: Transforming orthogonal inductive definition sets into confluent term rewrite systems