Proof Generation for Saturating First-Order Theorem Provers

          Stephan Schulz and Geoff Sutcliffe

We provide an overview of the state of the art (with some historical
context) with respect to the generation and representation of explicit
proof object from saturating first-order theorem provers. We discuss
some of the difficulties of the process and some of the uses and added
value of proof objects.