On the logic of unification

DOI10.1016/S0747-7171(89)80024-0MaRDI QIDQ1823935zbMATH OpenFDO

Authors Philippe le Chenadec

Publication date 1989

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

zbMATH Keywords

normalizationelimination ruleoperational semanticsconstructive type theoryrewriting systemequational logicmodel-theoretic semanticshigher-order unificationunification logic

Mathematics Subject Classification ID

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

Recommendations

• On the unity of logic
• On the logic of UNITY
• Unification in modal logic
• Unification in epistemic logics
• Algebraic and logical aspects of unification
• Unification in intuitionistic logic
• scientific article; zbMATH DE number 4071154
• UNIFICATION IN INTERMEDIATE LOGICS
• Unification types in logic

Cites work

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

Cited in

(10)

• Unification and Logarithmic Space
• Source-tracking unification
• The functional interpretation of direct computations
• Type inference in polymorphic type discipline
• Natural Deduction for Equality: The Missing Entity
• The unity of a Tractarian fact
• Unirationality of Ueno-Campana's threefold
• The logic of unification in grammar
• Algebraic and logical aspects of unification
• On the logic of UNITY

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1823935)