Intelligent backtracking in deduction systems by means of extended unification graphs
type: Item
instance of: scholarly article
title: Intelligent backtracking in deduction systems by means of extended unification graphs
zbMATH Open document ID: 0642.68153
DOI: 10.1007/BF00246022
author: Werner Dilger
author: Agnes Janson
published in: Journal of Automated Reasoning
publication date: 1986-01-01T00:00:00Z
review text: A method for unification as the basis for intelligent backtracking in deduction systems is described. This method is based on the unification graphs introduced by Cox. In this paper, unification graphs are used in an extended form such that they represent all the information which can be gained from the unification constraints, i.e., the expression to be unified, their subterms which, as a consequence, are to be unified, the number of deduction steps which cause the unification of two terms, and the term-subterm relation as far as necessary. If a unification conflict occurs from this information, the deduction steps which have led to these conflicts can be determined and reset. This is done by searching for loop-free paths or loops with certain properties in the extended unification graph, according to the type of unification conflict. Algorithms for the handling of the unification graph and for the extraction of information from it are described and proved as correct.
Mathematics Subject Classification ID: 68T15
zbMATH DE Number: 4047181
zbMATH Keywords: theorem proving
zbMATH Keywords: deduction plans
zbMATH Keywords: backtracking
zbMATH Keywords: unification graphs
MaRDI profile type: Publication
full work available at URL: https://doi.org/10.1007/bf00246022
OpenAlex ID: W2015933292
description: scientific article; zbMATH DE number 4047181