Properties of substitutions and unifications
type: Item
instance of: scholarly article
title: Properties of substitutions and unifications
zbMATH Open document ID: 0589.68063
DOI: 10.1016/S0747-7171(85)80027-4
author: Elmar Eder
published in: Journal of Symbolic Computation
publication date: 1985-01-01T00:00:00Z
review text: Basic properties of the semigroup of substitutions in first-order logic are proved. The idempotent substitutions are shown to form a complete lattice modulo renaming of variables. Most general unifiers are characterized as suprema of appropriate sets of substitutions. Also weak unifiers are considered, including a criterion for the existence of most general weak unifiers.
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B10
zbMATH DE Number: 3947653
zbMATH Keywords: semigroup of substitutions in first-order logic
zbMATH Keywords: unifiers
MaRDI profile type: Publication
cites work: Q3954845
cites work: Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
cites work: An Efficient Unification Algorithm
cites work: Linear unification
cites work: Q5678447
cites work: A Machine-Oriented Logic Based on the Resolution Principle
cites work: The Concept of Weak Substitution in Theorem-Proving
Recommended article: Q3326880
Recommended article: Q3735703
Recommended article: Higher order unification via explicit substitutions
Recommended article: Axiomatisation of substitution
Recommended article: Unification via the \(\lambda s_e\)-style of explicit substitutions
Recommended article: Q4472187
Recommended article: Confluence properties of weak and strong calculi of explicit substitutions
Recommended article: Explicit substitutions and reducibility
Recommended article: Substitutions into propositional tautologies
description: scientific article; zbMATH DE number 3947653