×

zbMATH — the first resource for mathematics

Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem. (English) Zbl 0847.68106
Summary: There are many papers describing problems solved using the Boyer-Moore theorem prover, as well as papers describing new tools and functionalities added to it. Unfortunately, so far there has been no tutorial paper describing typical interaction that a user has with this system when trying to solve a nontrivial problem, including a discussion of issues that arise in these situations. In this paper, we aim to fill this gap by illustrating how we have proved an interesting theorem with the Boyer-Moore theorem prover: a formalization of the assertion that the arithmetic mean of a sequence of natural numbers is greater than or equal to their geometric mean. We hope that this report will be of value not only for (non-expert) users of this system, who can learn some approaches (and tricks) to use when proving theorems with it, but also for implementors of automated deduction systems. Perhaps our main point is that, at least in the case of Nqthm, the user can interact with the system without knowing much about how it works inside. This perspective suggests the development of theorem provers that allow interaction that is user oriented and not system developer oriented.

MSC:
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Software:
NQTHM; Nuprl; PREVAIL
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Basin, D. and Kaufmann, M.: The Boyer-Moore prover and Nuprl: An experimental comparison, in Proc. Workshop for Basic Research Action, Logical Frameworks, Antibes, France, May 1990. · Zbl 0799.68169
[2] Bevier, W., Hunt, W.Jr., Moore, J., and Young, W.: An approach to systems verification, J. Automated Reasoning 5 (1989), 411–428.
[3] Boyer, R. S. and Moore, J S.: A Computational Logic, Academic Press, 1979.
[4] Borrione, D., Pierre, L., Salem, A., and Ashraf, M.: Formal verification of VHDL descriptions in the PREVAIL environment, in IEEE Design and Test, June 1992. · Zbl 0794.68143
[5] Boyer, R. S. and Moore, J S.: Metafunctions: proving them correct and using them efficiently as new proof procedures, in R. S.Boyer and J S.Moore (eds), The Correctness Problem in Computer Science, Academic Press London, 1981.
[6] Boyer, R. S. and Moore, J S.: A Computational Logic Handbook, Academic Press, 1988.
[7] Boyer, R. S., Kaufmann, M., and Moore, J S.: The Boyer-Moore theorem prover and its interactive enhancement, Computers and Mathematics with Applications 29 (1995), 27–62. · Zbl 00718810 · doi:10.1016/0898-1221(94)00215-7
[8] Bundy, A.: Talk in Challenge Problems section of Workshop on the Automation of Proof by Mathematical Induction, co-sponsored by MInd and IndUS, July 11–12, 1993; at AAAI-93 11th National Conf. Artificial Intelligence, Washington DC, USA.
[9] Good, D. and Young, W.: Mathematical methods for digital systems development, in S. Prehn and W. J. Toetenel (eds), VDM’91 Formal Software Development Methods, Springer-Verlag Lecture Notes in Computer Science 552 (1991), 406–430.
[10] Johnson, S. and Nagle, J.: Pascal-F Verifier User’s Manual, Version 2, Ford Aerospace & Communications Corporation, Palo Alto, CA, 1986.
[11] Kaufmann, M.: A User’s Manual for an Interactive Enhancement to the Boyer-Moore Theorem Prover, Technical Report 19, Computational Logic, Inc., May 198815.
[12] Kaufmann, M.: Addition of Free Variables to the PC-NQTHM Interactive Enhancement of the Boyer-Moore Theorem Prover, Technical Report 42, Computational Logic, Inc., March 1990.15
[13] Kaufmann, M.: Response to FM91 Survey of Formal Methods: Nqthm and Pc-Nqthm, Technical Report 75, Computational Logic, Inc., March 1992.15
[14] Kaufmann, M.: An Assistant for Reading Nqthm Proof Output, Technical Report 85, Computational Logic, Inc., November 1992.15
[15] Kaufmann, M.: An example in NQTHM: Ramsey’s theorem, Internal Note 100, Computational Logic, Inc., November 1988.
[16] Kaufmann, M.: An instructive example for beginning users of the Boyer-Moore theorem prover, Internal Note 185, Computational Logic, Inc., April 1990.
[17] Kaufmann, M.: Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithm, J. Automated Reasoning 7, (1991), 109–158. · Zbl 0723.68072 · doi:10.1007/BF00249356
[18] Kaufmann, M.: An extension of the Boyer-Moore theorem prover to support first-order quantification, J. Automated Reasoning 9 (1992), 355–372. · Zbl 0784.68076 · doi:10.1007/BF00245295
[19] Pierre, L.: The formal proof of sequential circuits described in CASCADE using the Boyer-Moore theorem prover, in L. Claesen (ed.), Formal VLSI Correctness Verification, North-Holland, 1990.
[20] Stallman, R. M.: GNU EMACS Manual, 6th edn., Free Software Foundation, March 1987.
[21] Kaufmann, M. and Pecchiari, P.: Interaction with the Boyer-Moore Theorem Prover: A Tutorial Study Using the Arithmetic-Geometric Mean Theorem, Technical Report 100, Computational Logic, Inc., August 1994,15 and Technical Report 9409-01, IRST, August 1994.16 (Revised June 1995.) · Zbl 0847.68106
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.