An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting
summary
Isabelle/HOL formalizes co-rewrite pairs and integrates polynomial interpretations over negative integers, the weighted path order and the co-WPO variant so the verified certifier CeTA can check non-reachability proofs produced by tools. The development refactors the term-relation interface, implements executable sufficient checks, and ships a prototype that emits certifiable XML proofs. A counterexample shows a multiset-argument extension of WPO is unsound for co-rewrite pairs, and experiments yield eight new problems solvable by these orders. polynomial interpretations over non-positive integers
AI-written summary · about
chapters (10)
- 0:00Certification in term rewriting
- 2:25SAT certifier aim
- 4:34Term rewriting basics
- 7:04Automating non-reachability proofs
- 8:32Extending certifier with co-rewrite pairs
- 13:33Refactoring term relation interface
- 19:59Adding co-rewrite pairs
- 23:18Prototype tool for proofs
- 24:25Summary and results
- 25:32Q&A
related talks
31mCertification of Confluence- and Commutation-Proofs via Parallel Critical Pairs
21mChecking Equivalence in a Non-strict Language
32mVerifying Haskell's Rewrite Rules based on Polymorphic Rewriting Theory
29mCertifying Complexity Analysis
18mCompleteness of an Axiomatization of Graph Isomorphism via Graph Rewriting in Coq
15mVerifying and Improving Halide’s Term Rewriting System with Program Synthesis
21mVerifying term graph optimizations using Isabelle/HOL
17mFormalizing Determinacy of Concurrent Revisions