A proof theory for general unification
type: Item
instance of: scholarly article
title: A proof theory for general unification
zbMATH Open document ID: 0746.03011
author: Wayne Snyder
published in: Progress in Computer Science and Applied Logic
publication date: 1992-09-18T00:00:00Z
review text: The topic of this book is \(E\)-unification and higher-order unification as extensions of the Martelli-Monanari method. First, a survey of the method for standard unification using transformations on systems of equations is presented, as well as soundness and completeness results. Then, \(\S 4\) outlines basic results on \(E\)-unification and proves the completeness of the narrowing method. \(\S 5\) defines a new representation of equational proofs as certain sets of trees. These trees are used to prove soundness and completeness of certain sets of transformations. In \(\S 6\) soundness and completeness results for an improved set of transformations are shown using the concept of unfailing completion. \(\S 7\) provides a proof of soundness and completeness of a method for higher-order unification and completeness of the strategy of eager variable elemination.
reviewed by: Erica Melis
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 68T15
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 68-02
Mathematics Subject Classification ID: 03C05
Mathematics Subject Classification ID: 68W30
zbMATH DE Number: 52764
zbMATH Keywords: \(E\)-unification
zbMATH Keywords: higher-order unification
zbMATH Keywords: extensions of the Martelli- Monanari method
zbMATH Keywords: narrowing method
zbMATH Keywords: equational proofs
zbMATH Keywords: trees
zbMATH Keywords: transformations
zbMATH Keywords: unfailing completion
zbMATH Keywords: eager variable elemination
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 52764