登入選單

返回Google圖書搜尋

A Computational Logic

Robert S. BoyerJ Strother Moore

出版	Academic Press, 1979
主題	Mathematics / AppliedMathematics / Logic
ISBN	01212295059780121229504
URL	http://books.google.com.hk/books?id=h1FKAAAAIAAJ&hl=&source=gbs_api

註釋

A sketch of the theory and two simple examples; A precise definition of the theory; The correctness of a tautology-checker; An overview of how we prove theorems; Using type information to simplify formulas; Using axioms and lemmas as rewrite rules; Using definitions; Rewriting terms and simplifying clauses; Eliminating destructors; Using equalities; Generalization; Eliminating irrelevance; Induction and the analysis of recursive definitions; Formulating an induction scheme for a conjecture; Illustrations of our techniques via elementary number theory; The correctness of a simple optimizing expression compiler; The correctness of a fast string searching algorithm; The unique prime factorization theorem.