A saturation-based unification algorithm for higher-order rational patterns

DOI10.1145/3704265MaRDI QIDQ7027564zbMATH OpenFDO

Authors Zhibo Chen, Frank Pfenning

Publication date 14 February 2025

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1145/3704265

zbMATH Keywords

pattern unificationrational termsregular Böhm trees

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• scientific article; zbMATH DE number 6680140 (Why is no real title available?)
• scientific article; zbMATH DE number 1088036 (Why is no real title available?)
• scientific article; zbMATH DE number 2102733 (Why is no real title available?)
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A Machine-Oriented Logic Based on the Resolution Principle
• A coverage checking algorithm for LF
• A logical framework with higher-order rational (circular) terms
• A unification algorithm for typed \(\bar\lambda\)-calculus
• An Efficient Unification Algorithm
• Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• Nominal unification
• Proving termination with multiset orderings
• Regular Böhm trees
• Representations of stream processors using nested fixed points
• Sequent calculi for induction and infinite descent
• Subtyping, declaratively. An exercise in mixed induction and coinduction
• The undecidability of unification in third order logic
• Well-founded recursion with copatterns and sized types

This page was built for publication: A saturation-based unification algorithm for higher-order rational patterns

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