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 92 articles )
Showing results 1 to 20 of 92.
Sorted by year (- Stratulat, Sorin: Mechanically certifying formula-based Noetherian induction reasoning (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)
- 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 \itdescente infinie -- 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)
- Krauss, Alexander: Partial and nested recursive function definitions in higher-order logic (2010)
- Medina-Bulo, Inmaculada; Palomo-Lozano, Francisco; Ruiz-Reina, José-Luis: A verified common lisp implementation of Buchberger’s algorithm in ACL2 (2010)
- Gamboa, Ruben A.: A formalization of powerlist algebra in ACL2 (2009)
- Geuvers, H.: Proof assistants: history, ideas and future (2009)
- Klein, Gerwin: Operating system verification---an overview (2009)
- L.Galdino, André; Ayala-Rincón, Mauricio: A PVS theory for term rewriting systems (2009)
- Wirth, Claus-Peter: Shallow confluence of conditional term rewriting systems (2009)
- Hesselink, Wim H.: Simulation refinement for concurrency verification (2008)