|
|
|---|
|
|
|
|---|
R. S. Boyer and J S. Moore, A Computational
Logic, Academic Press, 1979.
Relevance: implementation details of the prover that
became Nqthm
This book described the “Boyer-Moore theorem prover” as it
stood in 1979, when the prover was locally known as “Thm.” Unlike
the Edinburgh Pure Lisp Theorem Prover (PLTP), Thm supported datatypes other
than pairs, well-founded ordinals, a conservative definitional principle, and
named previously proved lemmas stored as rules. Unlike the later Nqthm, Thm
did not support
One outstanding feature of A Computational Logic was noted by Boyer and Moore in the Preface to the First Edition of bib::bm97 “we know of three independent successful efforts to construct the theorem prover from the book.” If you want to a good idea of how Nqthm and ACL2 “work,” read this book!