The undecidability of unification in third order logic

DOI10.1016/S0019-9958(73)90301-XMaRDI QIDQ5672888zbMATH OpenOpenAlexDBLPWikidataFDO

Authors 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

Decidability of theories and sets of sentences (03B25)

Cited in

(32)

• A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
• A unification algorithm for second-order monadic terms
• The undecidability of the second-order unification problem
• Unification under a mixed prefix
• A unification algorithm for typed \(\bar\lambda\)-calculus
• A unification algorithm for typed -calculus
• Mechanizing \(\omega\)-order type theory through unification
• 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
• Higher order unification via explicit substitutions
• On the undecidability of second-order unification
• Functions-as-constructors higher-order unification: extended pattern unification
• Mechanized metatheory revisited
• Higher-order unification via combinators
• Extensional higher-order paramodulation in Leo-III
• The inverse lambda calculus algorithm for typed first order logic lambda calculus and its application to translating English to FOL
• Unification for -calculi without propagation rules
• The undecidability of the D_A-unification problem
• Automatic theorem proving. II
• Decidability of the unification problem for second-order languages with unary functional symbols
• Typed answer set programming lambda calculus theories and correctness of inverse lambda algorithms with respect to them
• Linear second-order unification
• Nominal anti-unification modulo equational theories
• A saturation-based unification algorithm for higher-order rational patterns
• One is all you need: associative second-order unification without first-order variables
• Nominal equational narrowing: rewriting for unification in languages with binders
• Canonical for automated theorem proving in Lean
• Types, Tableaus and Gödel’s God in Isabelle/HOL
• Simple second-order languages for which unification is undecidable
• Steps toward a computational metaphysics
• Conditional equational theories and complete sets of transformations

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

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