Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms
Proceedings of the Sixth International Joint Conference on Artificial Intelligence. .
Abstract
A large number of axioms are often involved in the proof of a single theorem in many realistic applications of mechanical theorem proving such as formal verification of programs whose program domains are determined by user-defined axioms. There, fully automatic proofs are unrealistic due to the obvious constraints though a powerful machine support is highly desired. It is suggested that some meaningful structuring of theories can ease the difficulties. Several strategies are proposed to enhance efficient interactive non-resolution proofs on hierarchicall y and modularly structured theories with many axioms. Use of such strategies is illustrated in their application to verification of hierarchical programs with abstraction mechanisms.
@inproceedings{ijcai1979p86,
title = {Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms},
author = {Honda, Michio and Nakajima, Reiji},
booktitle = {Proceedings of the Sixth International Joint Conference on
Artificial Intelligence, {IJCAI-79}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Bruce G. Buchanan},
year = {1979},
month = {8},
url = {https://ijcai.org/proceedings/1979/86},
}
TY - CPAPER TI - Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms AU - Honda, Michio AU - Nakajima, Reiji T2 - Proceedings of the Sixth International Joint Conference on Artificial Intelligence, IJCAI-79 PB - International Joint Conferences on Artificial Intelligence PY - 1979 UR - https://ijcai.org/proceedings/1979/86 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
