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

[Haniel Barbosa]

Hello,

I would like to participate in the group.

Best,

--
Haniel Barbosa
https://homepages.dcc.ufmg.br/~hbarbosa/

[Simon Cruanes]

Hi Clark, I'd also like to participate in the group.

[Jochen Hoenicke]

Hi,

I would also like to participate in the group. 

Best, 

  Jochen

Simon Cruanes <simon.cru...@m4x.org> schrieb am Fr., 6. Aug. 2021, 22:04:

Hi Clark, I'd also like to participate in the group.

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/9ED2060B-6570-4CCC-A5B7-636E2B90CF7E%40m4x.org.

[Viktor Kunčak]

I am also interested.

 (Replying to the list as requested...)

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAFOm5sTmR7U6ki%2BgWtjyx0OFmAorS_oJFEhQ%2B-EKiaOF8KiLuw%40mail.gmail.com.

[Martin]

Hello,

I'm also interested!

kind regards,
Martin

> <mailto:smt-lib+u...@googlegroups.com>.

> To view this discussion on the web visit
> https://groups.google.com/d/msgid/smt-lib/CAFOm5sTmR7U6ki%2BgWtjyx0OFmAorS_oJFEhQ%2B-EKiaOF8KiLuw%40mail.gmail.com

> <https://groups.google.com/d/msgid/smt-lib/CAFOm5sTmR7U6ki%2BgWtjyx0OFmAorS_oJFEhQ%2B-EKiaOF8KiLuw%40mail.gmail.com?utm_medium=email&utm_source=footer>.

>
> --
> You received this message because you are subscribed to the Google Groups
> "SMT-LIB" group.
> To unsubscribe from this group and stop receiving emails from it, send an email
> to smt-lib+u...@googlegroups.com

> <mailto:smt-lib+u...@googlegroups.com>.

> To view this discussion on the web visit

> https://groups.google.com/d/msgid/smt-lib/CAOaq1xfh1sbVjBnu2UWSAQmyjzvUiVXzJi59o2Ug9R7v%3DoYGJA%40mail.gmail.com
> <https://groups.google.com/d/msgid/smt-lib/CAOaq1xfh1sbVjBnu2UWSAQmyjzvUiVXzJi59o2Ug9R7v%3DoYGJA%40mail.gmail.com?utm_medium=email&utm_source=footer>.

[Philipp Ruemmer]

Hi all,

I’m also interested in joining!

Regards, Philipp

[Dejan Jovanović]

Hi Clark, 

I would like to join the working group.

Cheers, Dejan

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.

To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAFOm5sTmR7U6ki%2BgWtjyx0OFmAorS_oJFEhQ%2B-EKiaOF8KiLuw%40mail.gmail.com.

[Andrew Reynolds]

I’d like to join as well.

-Andy

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAO63et%3DrZ3WmowGa9yLEGFauPH_Sfaf1qxE8BoyyPoAHirKH2g%40mail.gmail.com.

[Andres Nötzli]

I would like to join as well.

Thanks,

Andres

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAGqSYv0oY798upf%2BQBVHSO%2BFvxK4wPUV3axDt41k%3D3q4TNLHMQ%40mail.gmail.com.

[Geoff Sutcliffe]

Please may I join in? Interoperability with tptp prrofs would be a plus.

Cheers,

Geoff

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAGqSYv0oY798upf%2BQBVHSO%2BFvxK4wPUV3axDt41k%3D3q4TNLHMQ%40mail.gmail.com.

[Cesare Tinelli]

Geoff,

Of course you may join :) 

Thanks for wanting to contribute. I am sure your experience on proof generation and checking in the context of TPTP will be quite useful.

Best,

Cesare

[Nikolaj Bjorner]

me too

--

You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/9bf51077-6986-4293-aeb9-bfa1d56467c1n%40googlegroups.com.

[Giles Reger]

Well now I feel a bit left out replying just to Clark last week.

 

It would definitely be interesting to see how a system like Vampire could fit into this landscape. We would also be a customer of SMT proofs, in the sense that we currently have a proof step in our proofs that says “Z3 says so, if you don’t believe us go ask them”. As of earlier today we can also say “This is the SMT-LIB problem we gave Z3” but that’s about it.

 

At the PDAR workshop at CADE we also discussed proofs within the context of parallel/distributed solves and it would be great if this aspect was incorporated into the discussion.

 

Cheers, Giles

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/BYAPR21MB12085F8435EAE47C0E156F8AC3F69%40BYAPR21MB1208.namprd21.prod.outlook.com.

[Cesare Tinelli]

Hi Giles,

Thanks for your comments. Integration in ATPs is certainly another goal that would be facilitated by a common proof language. Do let us know if you'd like to join the working group.

Cesare

[Giles Reger]

Hi Cesare,

 

Sorry for not being clearer. Yes, I’d like to join. I emailed Clark last week before replying to the list got very popular :)

 

Cheers, Giles

 

(A somewhat interesting but irrelevant point about what “reply to this email” means, I guess the default reply-to being set to the group should be a hint but I have an automatic aversion to replying to mailing lists for seemingly admin things… an aversion I am apparently avoiding now)

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/4b08c5a8-f170-4903-a6c5-97ae16273fa9n%40googlegroups.com.

[Viktor Kunčak]

Dear all,

Have complete type checkers for dependent types (with implicits) of

http://smtlib.cs.uiowa.edu/version3.shtml

been already built? How complex is such a thing?

Sorry if I missed a paper describing this or even a discussion on this list.

I'm asking partly because I recall CVC had predicate types

and developers at some point were very happy to not have them.

Is this somehow going to be simpler to maintain in practice because

of less automated subtyping?

  Viktor

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAFOm5sTmR7U6ki%2BgWtjyx0OFmAorS_oJFEhQ%2B-EKiaOF8KiLuw%40mail.gmail.com.

[Simon Cruanes]

Hi Viktor,

I can't answer your question, but thanks for bringing attention to this
proposal that I didn't notice (at least not in its present form).
It looks pretty interesting, in particular because it moves from
implicit polymorphism with casts towards explicit polymorphism (with an
explicit application of polymorphic symbols to types… and terms)
with implicit parameters to be retrocompatible.

I have implemented solvers for polymorphic logics in the past, and I
found the explicit polymorphism approach to be much easier to handle
internally, so this proposal is imo a step in the right direction.

As for the subtyping predicates, yices 1 had it as well, I think, but
yices 2 also removed them.

--
Simon Cruanes

[Cesare Tinelli]

Dear member of the SMT community,

Thanks to all who have expressed their interest in joining a working group on SMT proofs. A mailing list was created a few months ago for the group:

smt-p...@googlegroups.com

While the the mailing list has been dormant for a while, there has been a flurry of activities on proof production and checking in several SMT groups, and a number of conversations have been started among members of these groups.

In an effort to move these conversations to the list and push the goals of the working group, Haniel Barbosa has kindly agreed to lead the working group.

He will follow up soon with some initial proposals on how to move forward.

Best,

Cesare,
also for Clark and Pascal

PS: If you are not in the working group yet and would like to join it, please send an email to Haniel (hbar...@dcc.ufmg.br) and he will add you to the mailing list.

--