First-Order Formative Rules

TL;DR

This paper introduces an improved first-order formative rules technique for term rewriting, simplifying termination proofs by reducing constraints, and adapting a higher-order concept to the first-order context.

Contribution

It adapts the formative rules method from higher-order to first-order term rewriting, enabling more efficient termination proofs.

Findings

Significant reduction in constraints during termination proofs

Enhanced technique for first-order term rewriting

Improved efficiency over previous methods

Abstract

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.