Pages that link to "Item:Q1150586"
From MaRDI portal
The following pages link to The undecidability of the second-order unification problem (Q1150586):
Displaying 50 items.
- The undecidability of simultaneous rigid E-unification (Q671659) (← links)
- Simple second-order languages for which unification is undecidable (Q807609) (← links)
- The lengths of proofs: Kreisel's conjecture and Gödel's speed-up theorem (Q843609) (← links)
- Simplifying the signature in second-order unification (Q843951) (← links)
- Expressing combinatory reduction systems derivations in the rewriting calculus (Q857913) (← links)
- Conditional equational theories and complete sets of transformations (Q918541) (← links)
- Generalizing proofs in monadic languages (with a postscript by Georg Kreisel). (Q930260) (← links)
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction (Q1075050) (← links)
- The number of proof lines and the size of proofs in first order logic (Q1102280) (← links)
- A unification algorithm for second-order monadic terms (Q1109019) (← links)
- Higher-order rewrite systems and their confluence (Q1127334) (← links)
- Equational unification, word unification, and 2nd-order equational unification (Q1129255) (← links)
- On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems (Q1164619) (← links)
- The undecidability of \(k\)-provability (Q1176199) (← links)
- Horn clause programs with polymorphic types: Semantics and resolution (Q1177936) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- A decision algorithm for distributive unification (Q1275018) (← links)
- Bounded arithmetic, proof complexity and two papers of Parikh (Q1295443) (← links)
- Typability and type checking in System F are equivalent and undecidable (Q1302292) (← links)
- Hybrid terms and sentences (Q1313083) (← links)
- Undecidable goals for completed acyclic programs (Q1326578) (← links)
- The Kreisel length-of-proof problem (Q1353977) (← links)
- Solvability of context equations with two context variables is decidable (Q1599536) (← links)
- On rewrite constraints and context unification (Q1607044) (← links)
- Farmer's theorem revisited (Q1607046) (← links)
- \(\forall \exists^{5}\)-equational theory of context unification is undecidable (Q1607219) (← links)
- Structuring and automating hardware proofs in a higher-order theorem- proving environment (Q1801500) (← links)
- A unification-theoretic method for investigating the \(k\)-provability problem (Q1814133) (← links)
- Complete sets of unifiers and matchers in equational theories (Q1820760) (← links)
- On the logic of unification (Q1823935) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- Logic with equality: Partisan corroboration and shifted pairing (Q1854299) (← links)
- Higher order unification via explicit substitutions (Q1854337) (← links)
- On the undecidability of second-order unification (Q1854349) (← links)
- Complexity of nilpotent unification and matching problems. (Q1854363) (← links)
- Decidability of bounded second order unification (Q1887168) (← links)
- Simultaneous rigid E-unification and other decision problems related to the Herbrand theorem (Q1960430) (← links)
- Proving theorems by reuse (Q1978233) (← links)
- Formalization of the computational theory of a Turing complete functional language model (Q2102949) (← links)
- Functions-as-constructors higher-order unification: extended pattern unification (Q2134936) (← links)
- The undecidability of proof search when equality is a logical connective (Q2134939) (← links)
- The undecidability of the second order predicate unification problem (Q2277244) (← links)
- Higher-order unification via combinators (Q2367541) (← links)
- Encoding abstract syntax without fresh names (Q2392477) (← links)
- Decidability of bounded higher-order unification (Q2456577) (← links)
- Higher-order unification: a structural relation between Huet's method and the one based on explicit substitutions (Q2480966) (← links)
- Referential logic of proofs (Q2500486) (← links)
- Tractable and intractable second-order matching problems (Q2643530) (← links)
- Nominal syntax with atom substitutions (Q2662669) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
