×

NQTHM

swMATH ID: 7543
Software Authors: Boyer, Robert S.; Moore, J. Strother
Description: A computational logic handbook. This book is a continuation of the same authors’ previous book entitled “A computational logic” (1979; Zbl 0448.68020). The truly important changes to the theorem prover since 1979 are the integration of a linear arithmetic decision procedure and the addition of a rather primitive facility permitting the user to give hints to the theorem prover. The significant changes in the logic itself are the efficient use of functions in the logic as new proof procedures upon the establishment of their soundness and the permission of bounded quantification and partial recursive functions. These changes in the logic were described completely in their “Metafunctions: proving them correct and using them efficiently as new proof procedures” [in “The correctness problem in computer science” (1981; Zbl 0476.68009)] and “The addition of bounded quantification and partial functions to a computational logic and its theorem prover” [J. Autom. Reasoning 4, No.2, 117-172 (1988)]. However, as a whole, there have been comparatively minor changes to the logic and the theorem prover since the publication of the authors’ former book, while the system has been applied to more and more difficult problems by more and more people. This book is intended as an updated thorough treatment of how to use the logic and the theorem prover.
Homepage: http://www.cs.utexas.edu/users/boyer/ftp/nqthm/
Keywords: functional programming; theorem prover; partial recursive functions
Related Software: HOL; ACL2; PVS; Coq; ML; Nuprl; Isabelle/HOL; Isabelle; LISP; RRL; UNITY; LCF; HOL Light; OTTER; ESC/Java; LARCH; CLAM; Cambridge LCF; Tecton; ETPS
Cited in: 139 Publications
Further Publications: ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html
all top 5

Cited by 180 Authors

13 Moore, J Strother
10 Hesselink, Wim H.
6 Kaufmann, Matt
5 Boyer, Robert S.
4 Russinoff, David M.
3 Armando, Alessandro
3 Bouhoula, Adel
3 Manolios, Panagiotis
3 Ranise, Silvio
3 Reddy, Uday S.
3 Walther, Christoph
2 Aubin, Raymond
2 Ayala-Rincón, Mauricio
2 Basin, David A.
2 Beeson, Michael J.
2 Bronsard, Francois
2 Claesen, Luc
2 Davis, Jared
2 De Man, H.
2 Dershowitz, Nachum
2 Farmer, William M.
2 Gamboa, Ruben A.
2 Geuvers, Jan Herman
2 Giunchiglia, Fausto
2 Hasker, Robert W.
2 Hennicker, Rolf
2 Jouannaud, Jean-Pierre
2 Kapur, Deepak
2 Kunen, Kenneth
2 Myreen, Magnus O.
2 Ray, Sandip
2 Schmaltz, Julien
2 Verkest, Diederik
2 Vroon, Daron
2 Waldmann, Uwe
2 Wang, Farn
2 Wirth, Claus-Peter
1 Al-Yahya, Tasniem Nasser
1 Alkassar, Eyad
1 Ammon, Kurt
1 Angelo, Catia M.
1 Baaz, Matthias
1 Ballarin, Clemens
1 Barnes, Janet
1 Bevier, William R.
1 Böhme, Sascha
1 Bolc, Leonard
1 Borowik, Piotr
1 Borrione, Dominique
1 Boulton, Richard J.
1 Bove, Ana
1 Bryant, Randal E.
1 Bundy, Alan
1 Burel, Guillaume
1 Bury, Guillaume
1 Cauderlier, Raphaël
1 Chapman, Roderick
1 Coglio, Alessandro
1 Cook, Andrew W.
1 Coquand, Thierry
1 Cowles, John R.
1 Cyrluk, David A.
1 de Groot, A. L.
1 Déharbe, David
1 Delahaye, David
1 Desharnais, Jules
1 Diallo, Nafi
1 Dillinger, Peter C.
1 Dybjer, Peter
1 Echenim, Mnacho
1 El-bachir Menai, Mohamed
1 Ellis, Bill J.
1 Felty, Amy P.
1 Fribourg, Laurent
1 Ganzinger, Harald
1 Gascard, Eric
1 Gedell, Tobias
1 Ghardallou, Wided
1 Goldschlag, David M.
1 Gramlich, Bernhard
1 Groote, Jan Friso
1 Guttman, Joshua D.
1 Hähnle, Reiner
1 Hajdú, Márton
1 Halmagrand, Pierre
1 Harman, N. A.
1 Hermant, Olivier
1 Hines, Larry M.
1 Howe, Douglas J.
1 Hozzová, Petra
1 Hua, Gary Xin
1 Huang, Chua-Huang
1 Huet, Gerard P.
1 Hunt, Warren A. jun.
1 Hurd, Joe
1 Hutter, Dieter
1 Ireland, Andrew
1 Jamnik, Mateja
1 Janičić, Predrag
1 Jiang, Yunfei
...and 80 more Authors

Citations by Year