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)

Full work available at URL https://doi.org/10.1016/S0747-7171(89)80024-0

zbMATH Keywords

constructive type theoryelimination ruleequational logichigher-order unificationmodel-theoretic semanticsnormalizationoperational semanticsrewriting systemunification 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)

Review text

The normalization process has been developed in various logics but was lacking in equational logic. The main explanation of this fact is the lack of an elimination rule in equational logic. However, this elimination is omnipresent in computer science in form of unification. Adding the new rule to the traditional introduction rule, the author obtains a unification logic LE with strong properties: atomicity of inferences, strict constructivism, strong normalization of deductions, left/right and introduction/elimination symmetries, positive/negative signatures for subexpression occurrences in deductions. The author gives two interpretations for unification logic. The first one is a model-theoretic semantics which gives completeness. The second one is the operational semantics of equational logic in a geometrical style. This semantics allows the design of a syntactical normalization process. This normalization result is obtained by a finite rewriting system. The relevance of this semantics and its operationality are clear also for the second-order level.

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

• 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
• 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?)
• 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)

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

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)