[SMT-COMP] New working group on SMT proofs

[Clark Barrett]

Dear SMT community,

As you know, producing independently checkable proofs has long been a
stretch goal for SMT solvers, with different solvers offering different
levels of support for such proofs and largely using independent formats.
Recently, there has been an increase in interest in this topic, both from
industry (e.g., Amazon's automated reasoning group) as well as from our own
community (e.g., the email thread started by Jochen Hoenicke following the
SMT competition).

As we have done in the past when various SMT topics have garnered
significant interest, we would like to propose creating a working group on
SMT proofs.  The purpose of the group is to make sure that many
perspectives are heard and considered and to develop a roadmap, within the
context of the overall SMT-LIB standard, that can hopefully synthesize a
variety of both short-term and long-term goals.

Please reply to this email if you would like to join the working group.  We
will aim to set up an initial discussion soon.

Best,

Clark Barrett, Pascal Fontaine, and Cesare Tinelli