Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms
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 hierarchically and modularly structured theories with many axioms. Use of such strategies is illustrated in their application to verification of hierarchical programs with abstraction mechanisms.
Cite
Text
Honda and Nakajima. "Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms." International Joint Conference on Artificial Intelligence, 1979.Markdown
[Honda and Nakajima. "Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms." International Joint Conference on Artificial Intelligence, 1979.](https://mlanthology.org/ijcai/1979/honda1979ijcai-interactive/)BibTeX
@inproceedings{honda1979ijcai-interactive,
title = {{Interactive Theorem Proving on Hierarchically and Modularly Structured Set of Very Many Axioms}},
author = {Honda, Michio and Nakajima, Reiji},
booktitle = {International Joint Conference on Artificial Intelligence},
year = {1979},
pages = {400-402},
url = {https://mlanthology.org/ijcai/1979/honda1979ijcai-interactive/}
}