The following pages link to (Q3343471):
Displaying 16 items.
- Simple second-order languages for which unification is undecidable (Q807609) (← links)
- On connections and higher-order logic (Q908896) (← links)
- A compact representation of proofs (Q1102282) (← links)
- A unification algorithm for second-order monadic terms (Q1109019) (← links)
- On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory (Q1120558) (← links)
- Unification theory (Q1124375) (← links)
- Unification under a mixed prefix (Q1201348) (← links)
- What holds in a context? (Q1312161) (← links)
- Set theory for verification. I: From foundations to functions (Q1319386) (← links)
- The foundation of a generic theorem prover (Q1823013) (← links)
- Higher-order unification revisited: Complete sets of transformations (Q1823936) (← links)
- Extensional higher-order paramodulation in Leo-III (Q2666959) (← links)
- Higher-order unification with dependent function types (Q5055716) (← links)
- Set-of-support strategy for higher-order logic (Q5881215) (← links)
- Higher-order unification, polymorphism, and subsorts (Q5881304) (← links)
- A Survey of the Proof-Theoretic Foundations of Logic Programming (Q6063891) (← links)
