Formalizing Soundness and Completeness of Unravelings

DOI10.1007/978-3-319-24246-0_15zbMath1471.68321OpenAlexW2293412579MaRDI QIDQ2964466

René Thiemann, Sarah Winkler

Publication date: 27 February 2017

Published in: Frontiers of Combining Systems (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-24246-0_15

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Formalization of mathematics in connection with theorem provers (68V20)

Uses Software

• Isabelle
• TALP
• AProVE
• Conditional Confluence
• ConCon

Cites Work

• Operational termination of conditional term rewriting systems
• Proving operational termination of membership equational programs
• Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity
• Unravelings and ultra-properties
• Certification of Termination Proofs Using CeTA
• Proving Termination of Programs Automatically with AProVE
• Term Rewriting and All That
• Conditional Confluence (System Description)
• Termination of logic programs: Transformational methods revisited
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Formalizing Soundness and Completeness of Unravelings