The undecidability of unification in third order logic

DOI10.1016/S0019-9958(73)90301-XzbMath0257.02038OpenAlexW2023266231WikidataQ55880674 ScholiaQ55880674MaRDI QIDQ5672888

Gérard Huet

Publication date: 1973

Published in: Information and Control (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s0019-9958(73)90301-x

Mathematics Subject Classification ID

Related Items (26)

Higher-order unification via combinators ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ The Inverse Lambda Calculus Algorithm for Typed First Order Logic Lambda Calculus and Its Application to Translating English to FOL ⋮ Linear second-order unification ⋮ Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ A unification algorithm for second-order monadic terms ⋮ The undecidability of the D_A-unification problem ⋮ Steps toward a computational metaphysics ⋮ Extensional higher-order paramodulation in Leo-III ⋮ The undecidability of the second-order unification problem ⋮ Conditional equational theories and complete sets of transformations ⋮ Automatic theorem proving. II ⋮ Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them ⋮ Unification under a mixed prefix ⋮ A unification algorithm for typed \(\bar\lambda\)-calculus ⋮ A unification algorithm for typed \(\overline\lambda\)-calculus ⋮ Mechanizing \(\omega\)-order type theory through unification ⋮ Decidability of the unification problem for second-order languages with unary functional symbols ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ Complete sets of unifiers and matchers in equational theories ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ Mechanized metatheory revisited ⋮ Higher order unification via explicit substitutions ⋮ On the undecidability of second-order unification ⋮ Simple second-order languages for which unification is undecidable ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

This page was built for publication: The undecidability of unification in third order logic