Termination orderings for rippling

DOI10.1007/3-540-58156-1_34zbMath1433.68187OpenAlexW1504895903MaRDI QIDQ5210791

Toby Walsh, David A. Basin

Publication date: 21 January 2020

Published in: Automated Deduction — CADE-12 (Search for Journal in Brave)

Full work available at URL: http://hdl.handle.net/11858/00-001M-0000-0014-B553-F

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items (2)

A calculus for and termination of rippling ⋮ Higher-order annotated terms for proof search

Uses Software

• CLAM
• Oyster

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Orderings for term-rewriting systems
• Rippling: A heuristic for guiding inductive proofs
• Termination of rewriting
• Productive use of failure in inductive proof
• Proving termination with multiset orderings
• Extensions to the rippling-out tactic for guiding inductive proofs
• Guiding induction proofs
• The OYSTER-CLAM system

This page was built for publication: Termination orderings for rippling