Mechanizing \(\omega\)-order type theory through unification

DOI10.1016/0304-3975(76)90021-9zbMath0361.02020MaRDI QIDQ1239309

D. C. Jensen, Tomasz Pietrzykowski

Publication date: 1977

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(76)90021-9

Mathematics Subject Classification ID

Related Items

On connections and higher-order logic, Unification under a mixed prefix, A unification algorithm for typed \(\bar\lambda\)-calculus, A unification algorithm for typed \(\overline\lambda\)-calculus, A higher-order unification algorithm for inductive types and dependent types, Complete sets of unifiers and matchers in equational theories, Higher-order unification revisited: Complete sets of transformations, The linked conjunct method for automatic deduction and related search techniques, Higher-order unification via combinators, Decidability of bounded higher-order unification, Automatic theorem proving. II, Decidability of the unification problem for second-order languages with unary functional symbols, Completeness, invariance and λ-definability

Cites Work

• A unification algorithm for typed \(\overline\lambda\)-calculus
• A Machine-Oriented Logic Based on the Resolution Principle
• Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems
• Resolution in type theory
• A Complete Mechanization of Second-Order Type Theory
• The undecidability of unification in third order logic
• Completeness in the theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item