Completion for unification

DOI10.1016/0304-3975(91)90182-2MaRDI QIDQ1178701zbMATH OpenOpenAlexFDO

Authors Narjes Doggaz, Claude Kirchner

Publication date 26 June 1992

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/0304-3975(91)90182-2

zbMATH Keywords

mergingmutationsyntactic theoryunification

Mathematics Subject Classification ID

Logic programming (68N17) Artificial intelligence (68T99)

Review text

This is an elaboration of a method of constructing unification algorithms for specific classes of equational theories proposed by the second author [Computing unification algorithms, Proc. 1st Symp. on Logic in Computer Science, Boston, 206-216 (1986)]. In particular, a completion procedure is developed which, if it terminates, transforms a set of linear axioms of a theory \(A\) into a presentation of \(A\) in resolvent form, from which a unification algorithm can be derived automatically.

Recommendations

• Complete equational unification based on an extension of the Knuth-Bendix completion procedure
• scientific article; zbMATH DE number 4049130
• Combining unification algorithms
• scientific article; zbMATH DE number 3866609

Cites work

• A complete proof of correctness of the Knuth-Bendix completion algorithm
• A Machine-Oriented Logic Based on the Resolution Principle
• A Unification Algorithm for Associative-Commutative Functions
• An Efficient Unification Algorithm
• scientific article; zbMATH DE number 3871320 (Why is no real title available?)
• scientific article; zbMATH DE number 3871322 (Why is no real title available?)
• scientific article; zbMATH DE number 4041327 (Why is no real title available?)
• scientific article; zbMATH DE number 4041328 (Why is no real title available?)
• scientific article; zbMATH DE number 4090765 (Why is no real title available?)
• scientific article; zbMATH DE number 3688776 (Why is no real title available?)
• scientific article; zbMATH DE number 3784848 (Why is no real title available?)
• scientific article; zbMATH DE number 3567992 (Why is no real title available?)
• scientific article; zbMATH DE number 3622985 (Why is no real title available?)
• scientific article; zbMATH DE number 3299786 (Why is no real title available?)
• scientific article; zbMATH DE number 3413831 (Why is no real title available?)
• THE PROBLEM OF SOLVABILITY OF EQUATIONS IN A FREE SEMIGROUP
• Varieties of ”If-Then-Else“

Cited in

(6)

• Partial completion of equational theories
• Abstract canonical presentations
• scientific article; zbMATH DE number 176128 (Why is no real title available?)
• Stream fusion, to completeness
• Linear completion
• Complete equational unification based on an extension of the Knuth-Bendix completion procedure

This page was built for publication: Completion for unification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1178701)