Efficient Full Higher-Order Unification
We developed a procedure to enumerate complete sets of higher-order unifiers based on work by Jensen and Pietrzykowski. Our procedure removes many redundant unifiers by carefully restricting the search space and tightly integrating decision procedures for fragments that admit a finite complete set o...
Main Authors: | Petar Vukmirović, Alexander Bentkamp, Visa Nummelin |
---|---|
Format: | Article |
Language: | English |
Published: |
Logical Methods in Computer Science e.V.
2021-12-01
|
Series: | Logical Methods in Computer Science |
Subjects: | |
Online Access: | https://lmcs.episciences.org/6919/pdf |
Similar Items
-
SAT-Inspired Higher-Order Eliminations
by: Jasmin Blanchette, et al.
Published: (2023-05-01) -
Superposition for Lambda-Free Higher-Order Logic
by: Alexander Bentkamp, et al.
Published: (2021-04-01) -
Exact Unification and Admissibility
by: George Metcalfe, et al.
Published: (2015-09-01) -
On Unification Modulo One-Sided Distributivity: Algorithms, Variants and Asymmetry
by: Andrew M Marshall, et al.
Published: (2015-06-01) -
On Higher-Order Probabilistic Subrecursion
by: Flavien Breuvart, et al.
Published: (2021-12-01)