A Computational Logic (1979)

Livro digital

Título:
A Computational Logic (1979)

Autor:
Robert S. Boyer, J Strother Moore

Categoria:
Tecnologia > Geral

Doador:
Raffaello D. N.

Sinopse:
A Computational Logic speaks to readers who want to see how automated reasoning actually works, not just what it promises. Its opening structure moves from motivation and proof techniques into a precise theory, then quickly into a mechanical theorem prover and a worked correctness proof for a tautology checker, grounding the subject in real machinery rather than abstraction alone. The table of contents shows a carefully staged progression: formal definitions, type information, rewrite rules, elimination of destructors, equalities, generalization, irrelevance, and induction. From there it expands into elementary number theory, then into a simple optimizing expression compiler, a fast string-searching algorithm, and finally the unique prime factorization theorem, with each chapter using the same logic engine in a different setting. This is a scholarly monograph by Robert S. Boyer and J Strother Moore, written for readers who want depth, not a tutorial gloss. The payoff is a clear view of the foundations of automated theorem proving, plus a sequence of substantial examples that reveal both the power and the discipline required to make computational logic work.