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