The undecidability of the second-order unification problem
From MaRDI portal
Publication:1150586
DOI10.1016/0304-3975(81)90040-2zbMath0457.03006OpenAlexW2059054133WikidataQ56092435 ScholiaQ56092435MaRDI QIDQ1150586
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
Undecidability and degrees of sets of sentences (03D35) Decidability of theories and sets of sentences (03B25) Applications of computability and recursion theory (03D80)
Related Items
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 DA-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
