An applicative multiset path order

DOI10.1007/978-3-032-32592-1_15MaRDI QIDQ7411310zbMATH OpenFDO

Authors Nao Hirokawa, Teppei Tanaka, Wataru Yachi

Publication date 2026

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/978-3-032-32592-1_15

zbMATH Keywords

path orderterm rewritingtermination

Mathematics Subject Classification ID

Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites work

• A Higher-Order Iterative Path Ordering
• A Lambda-Free Higher-Order Recursive Path Order
• A transfinite Knuth-Bendix order for lambda-free higher-order terms
• Analyzing program termination and complexity automatically with \textsf{AProVE}
• Comparing curried and uncurried rewriting
• Frontiers of Combining Systems
• Generalized and formalized uncurrying
• scientific article; zbMATH DE number 1301857 (Why is no real title available?)
• scientific article; zbMATH DE number 1889386 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• KBO orientability
• Nagoya termination tool
• Orderings for term-rewriting systems
• Polymorphic higher-order recursive path orderings
• Proof-theoretic analysis of termination proofs
• Proving termination with multiset orderings
• Rewrite-based Equational Theorem Proving with Selection and Simplification
• Rewriting Techniques and Applications
• SAT solving for termination proofs with recursive path orders and dependency pairs
• Term Rewriting and All That
• Term rewriting induction
• The computability path ordering
• The embedding path order for -free higher-order terms
• Uncurrying for termination and complexity

This page was built for publication: An applicative multiset path order

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q7411310)