Functions-as-constructors higher-order unification: extended pattern unification

DOI10.1007/S10472-021-09774-YMaRDI QIDQ2134936zbMATH OpenOpenAlexFDO

Authors Tomer Libal, Dale Miller

Publication date 4 May 2022

Published in Annals of Mathematics and Artificial Intelligence (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1007/s10472-021-09774-y

zbMATH Keywords

higher-order unificationdeterministic unification algorithmspattern unificationtype-free unification algorithms

Mathematics Subject Classification ID

Artificial intelligence (68Txx)

Recommendations

• Functions-as-constructors Higher-order Unification
• Two thoughts on higher-order unification -- most relevant unifiers and unification with case distinction
• Higher order E-unification
• Unification of higher-order patterns in linear time and space
• Unification with extended patterns

Cites work

• scientific article; zbMATH DE number 7471678 (Why is no real title available?)
• A Brief Overview of Agda – A Functional Language with Dependent Types
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A unification algorithm for Coq featuring universe polymorphism and overloading
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Abella: a system for reasoning about relational specifications
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Canonical Big Operators
• Crafting a Proof Assistant
• Deterministic second-order patterns
• Functions-as-constructors Higher-order Unification
• Higher-order dynamic pattern unification for dependent types and records
• Higher-order unification revisited: Complete sets of transformations
• Hints in Unification
• Implementing type theory in higher order constraint logic programming
• Isabelle/HOL. A proof assistant for higher-order logic
• Logic Based Program Synthesis and Transformation
• Programming with higher-order logic.
• Proof checking and logic programming
• Proving and applying program transformations expressed with second-order patterns
• Reasoning with higher-order abstract syntax in a logical framework
• Satallax: An Automatic Higher-Order Prover
• The lambda calculus. Its syntax and semantics. Rev. ed.
• The undecidability of the second-order unification problem
• The undecidability of unification in third order logic
• Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type
• Unification under a mixed prefix
• Unification with extended patterns

Cited in

(5)

• Feature generation using general constructor functions
• One or nothing: anti-unification over the simply-typed lambda calculus
• Logic Programming
• Sort-based confluence criteria for non-left-linear higher-order rewriting
• Functions-as-constructors Higher-order Unification

Describes a project that uses

Uses Software

• Teyjus
• Leo
• Agda
• Abella
• Twelf
• Satallax
• Isabelle/HOL
• Beluga
• TPS

This page was built for publication: Functions-as-constructors higher-order unification: extended pattern unification

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