A unification algorithm for second-order monadic terms

DOI10.1016/0168-0072(88)90015-2zbMATH Open0655.03004OpenAlexW2074213277MaRDI QIDQ1109019FDOQ1109019

Authors: William M. Farmer 

Publication date: 1988

Published in: Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0168-0072(88)90015-2

Recommendations

• The Complexity of Monadic Second-Order Unification
• Rewriting Techniques and Applications
• A parallel algorithm for the monadic unification problem
• scientific article; zbMATH DE number 2090082
• On the monadic second-order transduction hierarchy
• Monadic second-order logic, graph coverings and unfoldings of transition systems
• New algorithm for weak monadic second-order logic on inductive structures
• On Monadic Second-Order Theories of Multidominance Structures

zbMATH Keywords

algorithmunificationsecond-order terms

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Equational classes, universal algebra in model theory (03C05)

Cites Work

• Groups With Parametric Exponents
• An Efficient Unification Algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Title not available (Why is that?)
• Equations in Free Groups
• Proving and applying program transformations expressed with second-order patterns
• Title not available (Why is that?)
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Natural deduction as higher-order resolution
• The undecidability of the second-order unification problem
• Title not available (Why is that?)
• Title not available (Why is that?)
• The undecidability of unification in third order logic
• The Kreisel length-of-proof problem
• Title not available (Why is that?)

Cited In (23)

• Completion of rewrite systems with membership constraints
• \(\forall \exists^{5}\)-equational theory of context unification is undecidable
• The undecidability of \(k\)-provability
• Simplifying the signature in second-order unification
• Higher-order unification revisited: Complete sets of transformations
• On the undecidability of second-order unification
• Equational unification, word unification, and 2nd-order equational unification
• Regular patterns in second-order unification
• Tractable and intractable second-order matching problems
• Decidability of bounded second order unification
• Title not available (Why is that?)
• Title not available (Why is that?)
• Decidability of bounded higher-order unification
• Decidable higher-order unification problems
• Generalizing proofs in monadic languages (with a postscript by Georg Kreisel).
• Title not available (Why is that?)
• The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem
• Bounded arithmetic, proof complexity and two papers of Parikh
• Simple second-order languages for which unification is undecidable
• A unification-theoretic method for investigating the \(k\)-provability problem
• The Kreisel length-of-proof problem
• Some independence results for equational unification
• Second-order unification in the presence of linear shallow algebraic equations

This page was built for publication: A unification algorithm for second-order monadic terms

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