A Unification Algorithm for Second-Order Linear Terms
Gilles Dowek
TL;DR
This paper presents a specialized unification algorithm for second-order linear terms where each second-order variable appears only once, addressing a specific class of unification problems.
Contribution
It introduces a new unification algorithm tailored for second-order linear terms with single occurrences of variables, filling a gap in existing methods.
Findings
Algorithm successfully unifies second-order linear terms with single variable occurrences.
Proves correctness and termination of the proposed unification method.
Enhances understanding of second-order unification in restricted cases.
Abstract
We give an algorithm for the class of second order unification problems in which second order variables have at most one occurrence.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsPolynomial and algebraic computation