Unification of deterministic higher-order patterns

DOI10.1007/978-3-032-32592-1_12MaRDI QIDQ7411305zbMATH OpenFDO

Authors Aart Middeldorp

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_12

Mathematics Subject Classification ID

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

Cites work

• A formulation of the simple theory of types
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Deterministic second-order patterns
• Extensional higher-order paramodulation in Leo-III
• Functions-as-constructors higher-order unification: extended pattern unification
• Higher-order rewrite systems and their confluence
• Higher-order unification and matching
• Higher-order unification revisited: Complete sets of transformations
• Isabelle/HOL. A proof assistant for higher-order logic
• Linear unification of higher-order patterns
• Logic Based Program Synthesis and Transformation
• Mechanizing metatheory in a logical framework
• Superposition for higher-order logic
• TPS: A theorem-proving system for classical type theory

This page was built for publication: Unification of deterministic higher-order patterns

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