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