On the logic of unification
type: Item
instance of: scholarly article
title: On the logic of unification
zbMATH Open document ID: 0682.03033
DOI: 10.1016/S0747-7171(89)80024-0
published in: Journal of Symbolic Computation
publication date: 1989-01-01T00:00:00Z
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.
Mathematics Subject Classification ID: 03F35
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03F05
zbMATH DE Number: 4116523
zbMATH Keywords: constructive type theory
zbMATH Keywords: higher-order unification
zbMATH Keywords: normalization
zbMATH Keywords: elimination rule
zbMATH Keywords: unification logic
zbMATH Keywords: model-theoretic semantics
zbMATH Keywords: operational semantics
zbMATH Keywords: equational logic
zbMATH Keywords: rewriting system
author: Philippe le Chenadec
reviewed by: Nail Zamov
MaRDI profile type: Publication
cites work: Resolution in type theory
cites work: The lambda calculus, its syntax and semantics
cites work: Q3312256
cites work: Sequential algorithms on concrete data structures
cites work: The calculus of constructions
cites work: Fundamental properties of infinite trees
cites work: Q4772711
cites work: On the sequential nature of unification
cites work: Q3743300
cites work: Q5610986
cites work: Linear logic
cites work: Q3760480
cites work: The undecidability of the second-order unification problem
cites work: A unification algorithm for typed \(\overline\lambda\)-calculus
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: Finite Definability of Number‐Theoretic Functions and Parametric Completeness of Equational Calculi
cites work: Q3992832
cites work: Unifiability is complete for co-N Log Space
cites work: An Efficient Unification Algorithm
cites work: Linear unification
cites work: Q4068054
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: Solving functional equations at higher types; some examples and some theorems
cites work: New Classes for Parallel Complexity: A Study of Unification and Other Complete Problems for P
cites work: Q4192669
Recommended article: On the unity of logic
Recommended article: On the logic of UNITY
Recommended article: Unification in modal logic
Recommended article: Unification in epistemic logics
Recommended article: Algebraic and logical aspects of unification
Recommended article: Unification in intuitionistic logic
Recommended article: Q3803296
Recommended article: UNIFICATION IN INTERMEDIATE LOGICS
Recommended article: Q3518429
description: scientific article; zbMATH DE number 4116523