Read more
The development of new and improved proof systems, proof formats and
proof search methods is one of the most essential goals of Logic. But
what is a proof? What makes a proof better than another? How can a
proof be found efficiently? How can a proof be used? Logicians from
different communities usually provide radically different answers to
such questions. Their principles may be folklore within their own
communities but are often unknown to outsiders.
This book provides a snapshot of the current state of the art in proof
search and proof production as implemented in contemporary automated
reasoning tools such as SAT-solvers, SMT-solvers, first-order and
higher-order automated theorem provers and proof assistants.
Furthermore, various trends in proof theory, such as the calculus of
inductive constructions, deduction modulo, deep inference,
foundational proof certificates and cut-elimination, are surveyed;
and applications of formal proofs are illustrated in the areas of
cryptography, verification and mathematical proof mining.
Experts in these topics were invited to present tutorials about proofs
during the Vienna Summer of Logic and the chapters in this book
reflect their tutorials. Therefore, each chapter is intended to be
accessible not only to experts but also to novice researchers
from all fields of Logic.
