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.

BibTeX

@inproceedings{CFCK-RTATLCA14,
  author    = "Carsten Fuhs and Cynthia Kop",
  title     = "First-Order Formative Rules",
  booktitle = "Proceedings of the Joint 25th International Conference on
               Rewriting Techniques and Applications and 12th
               International Conference on Typed Lambda Calculi and
               Applications",
  editor    = "Gilles Dowek",
  series    = "Lecture Notes in Computer Science (Advanced Research in
               Computing and Software Science)",
  volume    = 8560,
  pages     = "240--256",
  year      = 2014,
  doi       = "10.1007/978-3-319-08918-8_17"
}