Interactive theorem proving on hierarchically and modularly structured set of very many axioms
Michio Honda, Reiji Nakajima · International Joint Conference on Artificial Intelligence · 1979
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.