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 all top 5 Cited in 26 Serials 38 Journal of Automated Reasoning 16 Formal Aspects of Computing 11 Theoretical Computer Science 10 Journal of Symbolic Computation 5 Formal Methods in System Design 3 Artificial Intelligence 3 Annals of Mathematics and Artificial Intelligence 2 Acta Informatica 2 Science of Computer Programming 2 Information and Computation 2 Distributed Computing 2 Sādhanā 1 RAIRO, Informatique Théorique 1 Acta Scientiarum Naturalium Universitatis Jilinensis 1 Journal of Computer Science and Technology 1 International Journal of Foundations of Computer Science 1 Archive for Mathematical Logic 1 Indagationes Mathematicae. New Series 1 Journal of Applied Non-Classical Logics 1 Documenta Mathematica 1 Logic Journal of the IGPL 1 LMS Journal of Computation and Mathematics 1 IEEE Annals of the History of Computing 1 The Journal of Logic and Algebraic Programming 1 Journal of Applied Logic 1 Journal of Logical and Algebraic Methods in Programming all top 5 Cited in 12 Fields 137 Computer science (68-XX) 35 Mathematical logic and foundations (03-XX) 4 Information and communication theory, circuits (94-XX) 3 General and overarching topics; collections (00-XX) 3 History and biography (01-XX) 2 Combinatorics (05-XX) 1 Number theory (11-XX) 1 Commutative algebra (13-XX) 1 Group theory and generalizations (20-XX) 1 Convex and discrete geometry (52-XX) 1 Numerical analysis (65-XX) 1 Operations research, mathematical programming (90-XX) Citations by Year