An Extension of Unification to Substitution with an Application to Automatic Theorem Proving
Abstract
The notion of unfiability is extended to substitutions. Theorems concerning this notion are derived together withan algorithm for computing the most general unifier of a set of substitutions. Especially fruitfull is the application in the case of the and-or tree approach to theorem proving where the subgoals are not independent but contain the same variables. Here the ultimate solution is shown to be the most general instance of the solutions to the individual subproblems. Another applications concerns connection graphs where the arcs are substitutions and new arcs can be generated from old arcs
Cite
Text
van Vaalen. "An Extension of Unification to Substitution with an Application to Automatic Theorem Proving." International Joint Conference on Artificial Intelligence, 1975.Markdown
[van Vaalen. "An Extension of Unification to Substitution with an Application to Automatic Theorem Proving." International Joint Conference on Artificial Intelligence, 1975.](https://mlanthology.org/ijcai/1975/vanvaalen1975ijcai-extension/)BibTeX
@inproceedings{vanvaalen1975ijcai-extension,
title = {{An Extension of Unification to Substitution with an Application to Automatic Theorem Proving}},
author = {van Vaalen, J.},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1975},
pages = {77-82},
url = {https://mlanthology.org/ijcai/1975/vanvaalen1975ijcai-extension/}
}