Publisher's Synopsis
An advanced, graduate-level text, surveying computational logic andset theory and its application to proof verification techniques. Bookdevelops all needed theory and provides a CD-ROM with a proof-verifierprogram to demonstrate concepts.Advanced CS students and researches will find the book an essentialpresentation 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 beexploited to model and carry out reasoning in branches of computerscience and mathematics*Provides a verifier aimed at tackling large-scale proof scenarios*Integrates important proof-engineering issues, reflecting the goalsof large-scale verifiers.
