On the logic of unification

DOI10.1016/S0747-7171(89)80024-0zbMath0682.03033MaRDI QIDQ1823935

Philippe le Chenadec

Publication date: 1989

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

zbMATH Keywords

operational semanticsequational logicnormalizationconstructive type theoryrewriting systemhigher-order unificationelimination rulemodel-theoretic semanticsunification logic

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Cut-elimination and normal-form theorems (03F05) Second- and higher-order arithmetic and fragments (03F35)

Related Items (4)

Type inference in polymorphic type discipline ⋮ The Functional Interpretation of Direct Computations ⋮ Source-tracking unification ⋮ Natural Deduction for Equality: The Missing Entity

Cites Work

• Linear logic
• Fundamental properties of infinite trees
• Solving functional equations at higher types; some examples and some theorems
• The calculus of constructions
• The undecidability of the second-order unification problem
• The lambda calculus, its syntax and semantics
• Sequential algorithms on concrete data structures
• Unifiability is complete for co-N Log Space
• A unification algorithm for typed \(\overline\lambda\)-calculus
• Linear unification
• On the sequential nature of unification
• Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
• An Efficient Unification Algorithm
• New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
• A Machine-Oriented Logic Based on the Resolution Principle
• Resolution in type theory
• Finite Definability of Number‐Theoretic Functions and Parametric Completeness of Equational Calculi
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: On the logic of unification