On the logic of unification (Q1823935)

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.