The undecidability of the second-order unification problem

DOI10.1016/0304-3975(81)90040-2zbMath0457.03006OpenAlexW2059054133WikidataQ56092435 ScholiaQ56092435MaRDI QIDQ1150586

Warren D. Goldfarb

Publication date: 1981

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(81)90040-2

zbMATH Keywords

common instance

Mathematics Subject Classification ID

Related Items (83)

Undecidable goals for completed acyclic programs ⋮ Higher-order unification, polymorphism, and subsorts ⋮ Higher-order unification via combinators ⋮ Linear unification of higher-order patterns ⋮ Functions-as-constructors higher-order unification: extended pattern unification ⋮ The undecidability of proof search when equality is a logical connective ⋮ Decidability of bounded second order unification ⋮ Validating Mathematical Structures ⋮ The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem ⋮ Simplifying the signature in second-order unification ⋮ Higher-order unification with dependent function types ⋮ Modular higher-order E-unification ⋮ Some independence results for equational unification ⋮ An algorithm for distributive unification ⋮ Linear second-order unification ⋮ Unification of higher-order patterns in a simply typed lambda-calculus with finite products and terminal type ⋮ Unification for $$\lambda $$ -calculi Without Propagation Rules ⋮ The Kreisel length-of-proof problem ⋮ The number of proof lines and the size of proofs in first order logic ⋮ Tractable and intractable second-order matching problems ⋮ Expressing combinatory reduction systems derivations in the rewriting calculus ⋮ A unification algorithm for second-order monadic terms ⋮ Encoding abstract syntax without fresh names ⋮ Nominal Unification and Matching of Higher Order Expressions with Recursive Let ⋮ The undecidability of the D_A-unification problem ⋮ Nominal syntax with atom substitutions ⋮ Higher-order rewrite systems and their confluence ⋮ Meeting of the Association for Symbolic Logic, Stanford, California, 1985 ⋮ Extensional higher-order paramodulation in Leo-III ⋮ Equational unification, word unification, and 2nd-order equational unification ⋮ Modular AC unification of higher-order patterns ⋮ Higher order disunification: Some decidable cases ⋮ On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems ⋮ Conditional equational theories and complete sets of transformations ⋮ Automatic theorem proving. II ⋮ Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem ⋮ Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). ⋮ The undecidability of \(k\)-provability ⋮ Horn clause programs with polymorphic types: Semantics and resolution ⋮ Decidability of bounded higher-order unification ⋮ Proving theorems by reuse ⋮ The undecidability of simultaneous rigid E-unification ⋮ Higher-Order Dynamic Pattern Unification for Dependent Types and Records ⋮ Graph unification and matching ⋮ The variable containment problem ⋮ Unification and matching modulo nilpotence ⋮ Unification under a mixed prefix ⋮ Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions ⋮ Analogy in Automated Deduction: A Survey ⋮ Codes and equations on trees ⋮ Asymptotic cyclic expansion and bridge groups of formal proofs ⋮ Referential logic of proofs ⋮ The undecidability of the second order predicate unification problem ⋮ Unnamed Item ⋮ Completion of rewrite systems with membership constraints ⋮ Inter-procedural Two-Variable Herbrand Equalities ⋮ Nominal Unification from a Higher-Order Perspective ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ Decidable higher-order unification problems ⋮ A unification-theoretic method for investigating the \(k\)-provability problem ⋮ Hilbert's Tenth Problem in Coq ⋮ A decision algorithm for distributive unification ⋮ Complete sets of unifiers and matchers in equational theories ⋮ F-ing modules ⋮ On the logic of unification ⋮ Higher-order unification revisited: Complete sets of transformations ⋮ On equality up-to constraints over finite trees, context unification, and one-step rewriting ⋮ Bounded arithmetic, proof complexity and two papers of Parikh ⋮ RIGID REACHABILITY, THE NON-SYMMETRIC FORM OF RIGID E-UNIFICATION ⋮ Typability and type checking in System F are equivalent and undecidable ⋮ Logic with equality: Partisan corroboration and shifted pairing ⋮ Higher order unification via explicit substitutions ⋮ On the undecidability of second-order unification ⋮ Complexity of nilpotent unification and matching problems. ⋮ Formalization of the computational theory of a Turing complete functional language model ⋮ Hybrid terms and sentences ⋮ Solvability of context equations with two context variables is decidable ⋮ Simple second-order languages for which unification is undecidable ⋮ On rewrite constraints and context unification ⋮ Farmer's theorem revisited ⋮ \(\forall \exists^{5}\)-equational theory of context unification is undecidable ⋮ Contextual equivalence for inductive definitions with binders in higher order typed functional programming ⋮ A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction

Cites Work

• Linear unification
• A Machine-Oriented Logic Based on the Resolution Principle
• The undecidability of unification in third order logic
• Some Results on the Length of Proofs

This page was built for publication: The undecidability of the second-order unification problem