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
- ISBN10 0387407626
- ISBN13 9780387407623
- Publish Date May 2005
- Publish Status Cancelled
- Out of Print 23 May 2007
- Publish Country US
- Imprint Springer-Verlag New York Inc.
- Edition 2004. Corr. 2nd Printing ed.
- Format Hardcover
- Pages 370
- Language English