Linear second-order unification

DOI10.1007/3-540-61464-8_63MaRDI QIDQ5055871zbMATH OpenOpenAlexFDO

Authors Jordi Levy

Publication date 9 December 2022

Published in Rewriting Techniques and Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/3-540-61464-8_63

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Recommendations

• Second-order unification in the presence of linear shallow algebraic equations
• A unification in the theory of linearization of second-order nonlinear ordinary differential equations
• Unranked second-order anti-unification
• Unranked second-order anti-unification
• Linear unification of higher-order patterns
• Regular patterns in second-order unification
• scientific article; zbMATH DE number 1615236
• On the linearization of second-order ordinary differential equations
• Decidability of bounded second order unification
• Unipodal algebra and 2nd-order linear differential equations

Cites work

• scientific article; zbMATH DE number 8800 (Why is no real title available?)
• scientific article; zbMATH DE number 1418812 (Why is no real title available?)
• A Complete Mechanization of Second-Order Type Theory
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• A termination ordering for higher order rewrite systems
• A unification algorithm for typed -calculus
• Bi-rewriting, a term rewriting technique for monotonic order relations
• Makanin's algorithm for word equations-two improvements and a generalization
• Mechanizing \(\omega\)-order type theory through unification
• The undecidability of the second-order unification problem
• The undecidability of unification in third order logic

Cited in

(17)

• Dominance constraints in stratified context unification
• On the undecidability of second-order unification
• Solvability of context equations with two context variables is decidable
• On rewrite constraints and context unification
• Regular patterns in second-order unification
• Decidability of bounded second order unification
• Tractable and intractable second-order matching problems
• scientific article; zbMATH DE number 2090082 (Why is no real title available?)
• On the relation between context and sequence unification
• On equality up-to constraints over finite trees, context unification, and one-step rewriting
• scientific article; zbMATH DE number 3896334 (Why is no real title available?)
• Decidability of bounded higher-order unification
• A decision algorithm for distributive unification
• Context unification with one context variable
• scientific article; zbMATH DE number 1615236 (Why is no real title available?)
• scientific article; zbMATH DE number 3870644 (Why is no real title available?)
• Second-order unification in the presence of linear shallow algebraic equations

This page was built for publication: Linear second-order unification

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