Unification under a mixed prefix

DOI10.1016/0747-7171(92)90011-RzbMath0768.68067MaRDI QIDQ1201348

S. Singh

Publication date: 17 January 1993

Published in: Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

unification; unifiers; raising; Skolemization; conjunctions of equations between simply typed \(\lambda\)-terms; mixed prefix; quantifier alternation

Mathematics Subject Classification ID

DB lookup for MSC labels failed

Uses Software

• Elf

Cites Work

• The undecidability of the second-order unification problem
• On the existence of closed terms in the typed lambda calculus II: Transformations of unification problems
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Mechanizing \(\omega\)-order type theory through unification
• Proving and applying program transformations expressed with second-order patterns
• Intuitionistic propositional logic is polynomial-space complete
• The foundation of a generic theorem prover
• Higher-order unification revisited: Complete sets of transformations
• Higher-order Horn clauses
• A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
• Natural deduction as higher-order resolution
• Higher-order unification with dependent function types
• Resolution in type theory
• A Complete Mechanization of Second-Order Type Theory
• The undecidability of unification in third order logic
• General models and extensionality
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item