NQTHM
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.
Keywords for this software
References in zbMATH (referenced in 149 articles )
Showing results 1 to 20 of 149.
Sorted by year (- Burel, Guillaume; Bury, Guillaume; Cauderlier, Raphaël; Delahaye, David; Halmagrand, Pierre; Hermant, Olivier: First-order automated reasoning with theories: when deduction modulo theory meets practice (2020)
- Echenim, M.; Peltier, N.: Combining induction and saturation-based theorem proving (2020)
- Kaufmann, Matt; Moore, J. Strother: Limited second-order functionality in a first-order setting (2020)
- Moore, J. Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
- Diallo, Nafi; Ghardallou, Wided; Desharnais, Jules; Mili, Ali: Convergence: integrating termination and abort-freedom (2018)
- Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
- Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (2017)
- Walther, Christoph; Wasser, Nathan: Fermat, Euler, Wilson -- three case studies in number theory (2017)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)
- Alkassar, Eyad; Böhme, Sascha; Mehlhorn, Kurt; Rizkallah, Christine: A framework for the verification of certifying computations (2014)
- Geuvers, Herman; Nederpelt, Rob: N. G. de Bruijn’s contribution to the formalization of mathematics (2013)
- Menai, Mohamed El Bachir; Al-Yahya, Tasniem Nasser: A taxonomy of exact methods for partial Max-SAT (2013)
- Ray, Sandip; Sumners, Rob: Specification and verification of concurrent programs through refinements (2013)
- Bove, Ana; Dybjer, Peter; Sicard-Ramírez, Andrés: Combining interactive and automatic reasoning in first order theories of functional programs (2012)
- Joswig, Michael: From Kepler to Hales, and back to Hilbert (2012)
- Verbeek, Freek; Schmaltz, Julien: Proof pearl: a formal proof of Dally and Seitz’ necessary and sufficient condition for deadlock-free routing in interconnection networks (2012)
- Wirth, Claus-Peter: Computer-assisted human-oriented inductive theorem proving by \textitdescenteinfinie -- a manifesto (2012)
- Hesselink, Wim H.: Simulation refinement for concurrency verification (2011)
- Myreen, Magnus O.; Davis, Jared: A verified runtime for a verified theorem prover (2011)
- Galdino, André L.; Ayala-Rincón, Mauricio: A formalization of the Knuth-Bendix(-Huet) critical pair theorem (2010)
Further publications can be found at: ftp://ftp.cs.utexas.edu/pub/boyer/nqthm/nqthm-bibliography.html