Application of Automatic Transformations to Program Verification
Proceedings of the Seventh International Joint Conference on Artificial Intelligence. Theoretical Foundations. Pages 472-478.
Abstract
A technique for incorporating automatic transformations into processes such as the application of inference rules, subsumption, and demodulation provides a mechanism for improving search strategies for theorem proving problems arising from the field of program verification. The incorporation of automatic transformations into the inference process can alter the search space for a given problem and is particularly useful for problems having "broad" rather than "deep" proofs. The technique can also be used to permit the generation of inferences that might otherwise be blocked and to build some commutativity or associativity into the unification process. Appropriate choice of transformations and new literal clashing and unification algorithms for applying them showed significant improvement on several real problems according to several distinct c riteria.
@inproceedings{ijcai1981p91,
title = {Application of Automatic Transformations to Program Verification},
author = {Veroff, Robert and Henschen, Lawrence J.},
booktitle = {Proceedings of the Seventh International Joint Conference on
Artificial Intelligence, {IJCAI-81}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Roger C. Schank},
pages = {472--478},
year = {1981},
month = {8},
note = {Theoretical Foundations},
url = {https://ijcai.org/proceedings/1981/91},
}
TY - CPAPER TI - Application of Automatic Transformations to Program Verification AU - Veroff, Robert AU - Henschen, Lawrence J. T2 - Proceedings of the Seventh International Joint Conference on Artificial Intelligence, IJCAI-81 PB - International Joint Conferences on Artificial Intelligence PY - 1981 SP - 472 EP - 478 UR - https://ijcai.org/proceedings/1981/91 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
