Interaction with the Boyer-Moore theorem prover: A tutorial study using the arithmetic-geometric mean theorem
- 1 March 1996
- journal article
- Published by Springer Nature in Journal of Automated Reasoning
- Vol. 16 (1-2) , 181-222
- https://doi.org/10.1007/bf00244463
Abstract
No abstract availableKeywords
This publication has 8 references indexed in Scilit:
- Mathematical methods for digital systems developmentPublished by Springer Nature ,2005
- The Boyer-Moore theorem prover and its interactive enhancementComputers & Mathematics with Applications, 1995
- An extension of the Boyer-Moore Theorem Prover to support first-order quantificationJournal of Automated Reasoning, 1992
- Quantification in Nqthm: A Recognizer and Some Constructive ImplementationsPublished by Defense Technical Information Center (DTIC) ,1992
- Formal verification of VHDL descriptions in the Prevail environmentIEEE Design & Test of Computers, 1992
- The Boyer-Moore prover and Nuprl: an experimental comparisonPublished by Cambridge University Press (CUP) ,1991
- Generalization in the presence of free variables: A mechanically-checked correctness proof for one algorithmJournal of Automated Reasoning, 1991
- An approach to systems verificationJournal of Automated Reasoning, 1989