Computational Logic and Set Theory
Springer (Publisher)
1st Edition
Published on 1. April 2007
Book
Mixed media product
368 pages
978-0-387-40762-3 (ISBN)
Description
An advanced, graduate-level text, surveying computational logic and
set theory and its application to proof verification techniques. Book
develops all needed theory and provides a CD-ROM with a proof-verifier
program to demonstrate concepts.
Advanced CS students and researches will find the book an essential
presentation of the theoretical concepts of proof verification (i.e.,
proof checker) systems for large-scale software systems.
Topics and features:
*Describes in-depth how a specific first-order theory can be
exploited to model and carry out reasoning in branches of computer
science and mathematics
*Provides a verifier aimed at tackling large-scale proof scenarios
*Integrates important proof-engineering issues, reflecting the goals
of large-scale verifiers
set theory and its application to proof verification techniques. Book
develops all needed theory and provides a CD-ROM with a proof-verifier
program to demonstrate concepts.
Advanced CS students and researches will find the book an essential
presentation of the theoretical concepts of proof verification (i.e.,
proof checker) systems for large-scale software systems.
Topics and features:
*Describes in-depth how a specific first-order theory can be
exploited to model and carry out reasoning in branches of computer
science and mathematics
*Provides a verifier aimed at tackling large-scale proof scenarios
*Integrates important proof-engineering issues, reflecting the goals
of large-scale verifiers
More details
Series
Edition
1., Ed.
Language
English
Place of publication
New York, NY
United States
Target group
Advanced grad students, researchers
Illustrations
75
75 s/w Abbildungen, 75 s/w Zeichnungen
mit 1 CD-ROM
ISBN-13
978-0-387-40762-3 (9780387407623)
Schweitzer Classification
Content
* Introduction * Propositional and predicate-calculus preliminaries * More on the structure of the verifier system * Undecidability and unsolvability * Appendix: A student's encyclopedia of mathematical analysis