2014/04/30 by Carsten Fuhs, Cynthia Kop, Fuhs, Carsten +1
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · doi:10.48550/arxiv.1404.7695
openalex publication_date 2014/04/30 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
This paper discusses the method of formative rules for first-order term rewriting, which was previously defined for a higher-order setting. Dual to the well-known usable rules, formative rules allow dropping some of the term constraints that need to be solved during a termination proof. Compared to the higher-order definition, the first-order setting allows for significant improvements of the technique.