ISR 2024 – Track C
Tools in Rewriting
Lecturer
Nao Hirokawa Japan Advanced Institute of Science and Technology
Course Description
Software tools based on rewriting have widely been used in the areas of programming languages, automated deduction, and software verification. The aim of this course is to give an introduction to rewriting tools and their tool developments. We study their usage, underlying theories, and potential applications, giving a brief introduction to related tool competitions (such as REC, termCOMP, CoCo, and CASC) and standard formats.
We pick up the following four types of tools.
- Rewrite engines: After a brief introduction to algebraic specification languages (CafeOBJ/Maude), we discuss theory of rewriting modulo theories and implementation techniques for (AC) rewriting.
- Termination: We study the dependency pair method with interpretation orders for termination and runtime complexity analysis, discussing their easy SMT encodings. We also briefly discuss how programs are translated to rewrite systems.
- Confluence: Rule labeling and transformation/decomposition techniques are popular powerful methods in modern confluence tools. We study their background theories and automation techniques, discussing translation techniques from conditional rewrite systems to unconditional rewrite systems.
- Completion: Knuth–Bendix completion and ordered completion are theoretical foundations for automatic theorem provers. We study basics of these methods as well as recent techniques for finding suitable reduction orders by MaxSAT. In addition, we discuss the split-if translation that reduces the satisfiability problem of Horn clauses to a word problem.
Prerequisites
Basis knowledge about rewriting, algebras, recursive path orders, and critical pairs.