An Extension of Unification to Substitution with an Application to Automatic Theorem Proving
Proceedings of the Fourth International Joint Conference on Artificial Intelligence. Mathematical and Theoretical Aspects of A.I. Pages 77-81.
Abstract
The notion of unifiability is extended to substitutions. Theorems concerning this notion are derived together with an algorithm for computing the most general unifier of a set of substitutions.Especially fruitful! 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 application concerns connection graphs where the arcs are substitutions and new arcs can be generated from old arcs.
@inproceedings{ijcai1975p13,
title = {An Extension of Unification to Substitution with an Application to Automatic Theorem Proving},
author = {van Vaalen, J.},
booktitle = {Proceedings of the Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-75}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Patrick Winston and Carl Hewitt},
pages = {77--81},
year = {1975},
note = {Mathematical and Theoretical Aspects of A.I},
url = {https://ijcai.org/proceedings/1975/13},
}
TY - CPAPER TI - An Extension of Unification to Substitution with an Application to Automatic Theorem Proving AU - van Vaalen, J. T2 - Proceedings of the Fourth International Joint Conference on Artificial Intelligence, IJCAI-75 PB - International Joint Conferences on Artificial Intelligence PY - 1975 SP - 77 EP - 81 UR - https://ijcai.org/proceedings/1975/13 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
