Decidability of the unification problem for second-order languages with unary functional symbols

DOI10.1007/BF01071228zbMath0443.03009MaRDI QIDQ3885741

A. P. Zhezherun

Publication date: 1979

Published in: Cybernetics (Search for Journal in Brave)

zbMATH Keywords

unification problemsecond-order languages

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Mechanization of proofs and logical operations (03B35)

Related Items

Simplifying the signature in second-order unification ⋮ Decidability of bounded higher-order unification ⋮ On the undecidability of second-order unification

Cites Work

• Unnamed Item
• A unification algorithm for typed \(\bar\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• A Machine-Oriented Logic Based on the Resolution Principle
• A Complete Mechanization of Second-Order Type Theory
• The undecidability of unification in third order logic

This page was built for publication: Decidability of the unification problem for second-order languages with unary functional symbols