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...