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

DOI10.1016/0304-3975(76)90021-9zbMath0361.02020OpenAlexW1990121424MaRDI 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 (22)

Higher-order unification via combinators ⋮ Linear second-order unification ⋮ A higher-order unification algorithm for inductive types and dependent types ⋮ Superposition for higher-order logic ⋮ On connections and higher-order logic ⋮ Automatic theorem proving. II ⋮ Unnamed Item ⋮ Decidability of bounded higher-order unification ⋮ The CADE-27 Automated theorem proving System Competition – CASC-27 ⋮ Unification under a mixed prefix ⋮ A unification algorithm for typed \(\bar\lambda\)-calculus ⋮ A unification algorithm for typed \(\overline\lambda\)-calculus ⋮ Superposition with lambdas ⋮ Making higher-order superposition work ⋮ Making higher-order superposition work ⋮ Superposition with lambdas ⋮ Decidability of the unification problem for second-order languages with unary functional symbols ⋮ Superposition for full higher-order logic ⋮ 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 ⋮ Completeness, invariance and λ-definability

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• 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

This page was built for publication: Mechanizing \(\omega\)-order type theory through unification