One is all you need: associative second-order unification without first-order variables

DOI10.46298/LMCS-22(2:3)2026MaRDI QIDQ7254979zbMATH OpenFDO

Authors David M. Cerna, Julian Parsert

Publication date 29 May 2026

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.46298/LMCS-22(2:3)2026

Mathematics Subject Classification ID

Logic in computer science (03B70) Computer science (68-XX)

Cites work

• A combinatory logic approach to higher-order E-unification
• A direct proof of the finite developments theorem
• A unification algorithm for second-order monadic terms
• Context unification is in PSPACE
• Counterexample guided inductive synthesis modulo theories
• Decidability of bounded second order unification
• Equational unification, word unification, and 2nd-order equational unification
• Experiments on infinite model finding in SMT solving
• Extending SMT solvers to higher-order logic
• Higher order E-unification
• scientific article; zbMATH DE number 1302628 (Why is no real title available?)
• scientific article; zbMATH DE number 545277 (Why is no real title available?)
• Linear second-order unification
• Modular higher-order E-unification
• On the undecidability of second-order unification
• The Complexity of Monadic Second-Order Unification
• The structural \(\lambda \)-calculus
• The undecidability of the second-order unification problem
• The undecidability of unification in third order logic

This page was built for publication: One is all you need: associative second-order unification without first-order variables

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